Theorem fnmpoi 8016

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3430   × cxp 5622   Fn wfn 6487   ∈ cmpo 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  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 7364  df-mpo 7365  df-1st 7935  df-2nd 7936

This theorem is referenced by:  dmmpo  8017  fnoa  8436  fnom  8437  fnoe  8438  fnmap  8773  fnpm  8774  addpqnq  10852  mulpqnq  10855  mpoaddf  11123  mpomulf  11124  elq  12891  cnref1o  12926  ccatfn  14525  qnnen  16171  restfn  17378  prdsdsfn  17419  imasdsfn  17469  imasvscafn  17492  homffn  17650  comfffn  17661  comffn  17662  isoval  17723  cofucl  17846  fnfuc  17906  natffn  17910  catcisolem  18068  estrchomfn  18092  funcestrcsetclem4  18100  funcsetcestrclem4  18115  fnxpc  18133  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  yonedalem3  18237  yonedainv  18238  plusffn  18608  mulgfval  19036  mulgfvalALT  19037  mulgfn  19039  gimfn  19227  sylow2blem2  19587  rnghmfn  20410  rhmfn  20467  rnghmsscmap2  20597  rnghmsscmap  20598  rhmsscmap2  20626  rhmsscmap  20627  srhmsubc  20648  rhmsubclem1  20653  fldc  20752  fldhmsubc  20753  scaffn  20869  lmimfn  21013  ipffn  21641  mplsubrglem  21992  tx1stc  23625  tx2ndc  23626  hmeofn  23732  efmndtmd  24076  qustgplem  24096  nmoffn  24686  rrxmfval  25383  mbfimaopnlem  25632  i1fadd  25672  i1fmul  25673  subsfn  28030  ex-fpar  30547  smatrcl  33956  txomap  33994  qtophaus  33996  pstmxmet  34057  dya2icoseg  34437  dya2iocrfn  34439  fncvm  35455  mpomulnzcnf  36497  cntotbnd  38131  grimfn  48367  grlimfn  48467  rngchomffvalALTV  48766  rngchomrnghmresALTV  48767  rhmsubcALTVlem1  48769  funcringcsetcALTV2lem4  48781  funcringcsetclem4ALTV  48804  srhmsubcALTV  48813  fldcALTV  48820  fldhmsubcALTV  48821  rrx2xpref1o  49206  sectfn  49516  discsubclem  49550  oppffn  49611  swapf2fn  49755  fucofn2  49811  fucoppc  49897  functhinclem1  49931  lanfn  50096  ranfn  50097