Theorem fnmpoi 8094

Description: Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)

Hypotheses

Ref	Expression
fmpo.1	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
fnmpoi.2	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
fnmpoi	⊢ 𝐹 Fn (𝐴 × 𝐵)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem fnmpoi

Step	Hyp	Ref	Expression
1		fnmpoi.2	. . 3 ⊢ 𝐶 ∈ V
2	1	rgen2w 3064	. 2 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V
3		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 8093	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	ax-mp 5	1 ⊢ 𝐹 Fn (𝐴 × 𝐵)

Syntax hints:   = wceq 1537   ∈ wcel 2106  ∀wral 3059  Vcvv 3478   × cxp 5687   Fn wfn 6558   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014

This theorem is referenced by:  dmmpo  8095  fnoa  8545  fnom  8546  fnoe  8547  fnmap  8872  fnpm  8873  addpqnq  10976  mulpqnq  10979  mpoaddf  11247  mpomulf  11248  elq  12990  cnref1o  13025  ccatfn  14607  qnnen  16246  restfn  17471  prdsdsfn  17512  imasdsfn  17561  imasvscafn  17584  homffn  17738  comfffn  17749  comffn  17750  isoval  17813  cofucl  17939  fnfuc  18000  natffn  18004  catcisolem  18164  estrchomfn  18190  funcestrcsetclem4  18199  funcsetcestrclem4  18214  fnxpc  18232  1stfcl  18253  2ndfcl  18254  prfcl  18259  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  yonedalem3  18337  yonedainv  18338  plusffn  18675  mulgfval  19100  mulgfvalALT  19101  mulgfn  19103  gimfn  19292  sylow2blem2  19654  rnghmfn  20456  rhmfn  20516  rnghmsscmap2  20646  rnghmsscmap  20647  rhmsscmap2  20675  rhmsscmap  20676  srhmsubc  20697  rhmsubclem1  20702  fldc  20802  fldhmsubc  20803  scaffn  20898  lmimfn  21043  ipffn  21687  mplsubrglem  22042  tx1stc  23674  tx2ndc  23675  hmeofn  23781  efmndtmd  24125  qustgplem  24145  nmoffn  24748  rrxmfval  25454  mbfimaopnlem  25704  i1fadd  25744  i1fmul  25745  subsfn  28071  ex-fpar  30491  smatrcl  33757  txomap  33795  qtophaus  33797  pstmxmet  33858  dya2icoseg  34259  dya2iocrfn  34261  fncvm  35242  mpomulnzcnf  36282  cntotbnd  37783  grimfn  47803  grlimfn  47882  rngchomffvalALTV  48122  rngchomrnghmresALTV  48123  rhmsubcALTVlem1  48125  funcringcsetcALTV2lem4  48137  funcringcsetclem4ALTV  48160  srhmsubcALTV  48169  fldcALTV  48176  fldhmsubcALTV  48177  rrx2xpref1o  48568  functhinclem1  48841