Theorem fnmpoi 8047

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  ∀wral 3075  Vcvv 3453   × cxp 5643   Fn wfn 6512   ∈ cmpo 7394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-oprab 7396  df-mpo 7397  df-1st 7966  df-2nd 7967

This theorem is referenced by:  dmmpo  8048  fnoa  8472  fnom  8473  fnoe  8474  fnmap  8810  fnpm  8811  addpqnq  10893  mulpqnq  10896  mpoaddf  11164  mpomulf  11165  elq  12948  cnref1o  12983  ccatfn  14582  qnnen  16228  restfn  17436  prdsdsfn  17477  imasdsfn  17527  imasvscafn  17550  homffn  17708  comfffn  17719  comffn  17720  isoval  17781  cofucl  17904  fnfuc  17964  natffn  17968  catcisolem  18126  estrchomfn  18150  funcestrcsetclem4  18158  funcsetcestrclem4  18173  fnxpc  18191  1stfcl  18212  2ndfcl  18213  prfcl  18218  evlfcl  18237  curf1cl  18243  curfcl  18247  hofcl  18274  yonedalem3  18295  yonedainv  18296  plusffn  18666  mulgfval  19094  mulgfvalALT  19095  mulgfn  19097  gimfn  19284  sylow2blem2  19644  rnghmfn  20467  rhmfn  20527  rnghmsscmap2  20658  rnghmsscmap  20659  rhmsscmap2  20687  rhmsscmap  20688  srhmsubc  20709  rhmsubclem1  20714  fldc  20813  fldhmsubc  20814  scaffn  20930  lmimfn  21073  ipffn  21683  mplsubrglem  22035  tx1stc  23690  tx2ndc  23691  hmeofn  23797  efmndtmd  24141  qustgplem  24161  nmoffn  24751  rrxmfval  25448  mbfimaopnlem  25697  i1fadd  25737  i1fmul  25738  subsfn  28094  ex-fpar  30610  smatrcl  34054  txomap  34092  qtophaus  34094  pstmxmet  34155  dya2icoseg  34535  dya2iocrfn  34537  fncvm  35571  mpomulnzcnf  36623  cntotbnd  38259  grimfn  48465  grlimfn  48565  rngchomffvalALTV  48864  rngchomrnghmresALTV  48865  rhmsubcALTVlem1  48867  funcringcsetcALTV2lem4  48879  funcringcsetclem4ALTV  48902  srhmsubcALTV  48911  fldcALTV  48918  fldhmsubcALTV  48919  rrx2xpref1o  49304  sectfn  49614  discsubclem  49648  oppffn  49709  swapf2fn  49853  fucofn2  49909  fucoppc  49995  functhinclem1  50029  lanfn  50194  ranfn  50195