Theorem fnmpoi 8014

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 3056	. 2 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V
3		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 8013	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	ax-mp 5	1 ⊢ 𝐹 Fn (𝐴 × 𝐵)

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   × cxp 5622   Fn wfn 6487   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934

This theorem is referenced by:  dmmpo  8015  fnoa  8435  fnom  8436  fnoe  8437  fnmap  8770  fnpm  8771  addpqnq  10849  mulpqnq  10852  mpoaddf  11120  mpomulf  11121  elq  12863  cnref1o  12898  ccatfn  14495  qnnen  16138  restfn  17344  prdsdsfn  17385  imasdsfn  17435  imasvscafn  17458  homffn  17616  comfffn  17627  comffn  17628  isoval  17689  cofucl  17812  fnfuc  17872  natffn  17876  catcisolem  18034  estrchomfn  18058  funcestrcsetclem4  18066  funcsetcestrclem4  18081  fnxpc  18099  1stfcl  18120  2ndfcl  18121  prfcl  18126  evlfcl  18145  curf1cl  18151  curfcl  18155  hofcl  18182  yonedalem3  18203  yonedainv  18204  plusffn  18574  mulgfval  18999  mulgfvalALT  19000  mulgfn  19002  gimfn  19190  sylow2blem2  19550  rnghmfn  20375  rhmfn  20432  rnghmsscmap2  20562  rnghmsscmap  20563  rhmsscmap2  20591  rhmsscmap  20592  srhmsubc  20613  rhmsubclem1  20618  fldc  20717  fldhmsubc  20718  scaffn  20834  lmimfn  20978  ipffn  21606  mplsubrglem  21959  tx1stc  23594  tx2ndc  23595  hmeofn  23701  efmndtmd  24045  qustgplem  24065  nmoffn  24655  rrxmfval  25362  mbfimaopnlem  25612  i1fadd  25652  i1fmul  25653  subsfn  28020  ex-fpar  30537  smatrcl  33953  txomap  33991  qtophaus  33993  pstmxmet  34054  dya2icoseg  34434  dya2iocrfn  34436  fncvm  35451  mpomulnzcnf  36493  cntotbnd  37993  grimfn  48121  grlimfn  48221  rngchomffvalALTV  48520  rngchomrnghmresALTV  48521  rhmsubcALTVlem1  48523  funcringcsetcALTV2lem4  48535  funcringcsetclem4ALTV  48558  srhmsubcALTV  48567  fldcALTV  48574  fldhmsubcALTV  48575  rrx2xpref1o  48960  sectfn  49270  discsubclem  49304  oppffn  49365  swapf2fn  49509  fucofn2  49565  fucoppc  49651  functhinclem1  49685  lanfn  49850  ranfn  49851