Theorem fnmpoi 8052

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   × cxp 5639   Fn wfn 6509   ∈ cmpo 7392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972

This theorem is referenced by:  dmmpo  8053  fnoa  8475  fnom  8476  fnoe  8477  fnmap  8809  fnpm  8810  addpqnq  10898  mulpqnq  10901  mpoaddf  11169  mpomulf  11170  elq  12916  cnref1o  12951  ccatfn  14544  qnnen  16188  restfn  17394  prdsdsfn  17435  imasdsfn  17484  imasvscafn  17507  homffn  17661  comfffn  17672  comffn  17673  isoval  17734  cofucl  17857  fnfuc  17917  natffn  17921  catcisolem  18079  estrchomfn  18103  funcestrcsetclem4  18111  funcsetcestrclem4  18126  fnxpc  18144  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlfcl  18190  curf1cl  18196  curfcl  18200  hofcl  18227  yonedalem3  18248  yonedainv  18249  plusffn  18583  mulgfval  19008  mulgfvalALT  19009  mulgfn  19011  gimfn  19200  sylow2blem2  19558  rnghmfn  20355  rhmfn  20415  rnghmsscmap2  20545  rnghmsscmap  20546  rhmsscmap2  20574  rhmsscmap  20575  srhmsubc  20596  rhmsubclem1  20601  fldc  20700  fldhmsubc  20701  scaffn  20796  lmimfn  20940  ipffn  21567  mplsubrglem  21920  tx1stc  23544  tx2ndc  23545  hmeofn  23651  efmndtmd  23995  qustgplem  24015  nmoffn  24606  rrxmfval  25313  mbfimaopnlem  25563  i1fadd  25603  i1fmul  25604  subsfn  27937  ex-fpar  30398  smatrcl  33793  txomap  33831  qtophaus  33833  pstmxmet  33894  dya2icoseg  34275  dya2iocrfn  34277  fncvm  35251  mpomulnzcnf  36294  cntotbnd  37797  grimfn  47883  grlimfn  47982  rngchomffvalALTV  48270  rngchomrnghmresALTV  48271  rhmsubcALTVlem1  48273  funcringcsetcALTV2lem4  48285  funcringcsetclem4ALTV  48308  srhmsubcALTV  48317  fldcALTV  48324  fldhmsubcALTV  48325  rrx2xpref1o  48711  sectfn  49022  discsubclem  49056  oppffn  49117  swapf2fn  49261  fucofn2  49317  fucoppc  49403  functhinclem1  49437  lanfn  49602  ranfn  49603