Theorem fnmpoi 8071

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453   × cxp 5657   Fn wfn 6532   ∈ cmpo 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991

This theorem is used by:  dmmpo  8072  fnoa  8499  fnom  8500  fnoe  8501  fnmap  8836  fnpm  8837  addpqnq  10951  mulpqnq  10954  mpoaddf  11222  mpomulf  11223  elq  13003  cnref1o  13039  ccatfn  14641  qnnen  16307  restfn  17515  prdsdsfn  17556  imasdsfn  17606  imasvscafn  17629  homffn  17787  comfffn  17798  comffn  17799  isoval  17860  cofucl  17983  fnfuc  18043  natffn  18047  catcisolem  18205  estrchomfn  18229  funcestrcsetclem4  18237  funcsetcestrclem4  18252  fnxpc  18270  1stfcl  18291  2ndfcl  18292  prfcl  18297  evlfcl  18316  curf1cl  18322  curfcl  18326  hofcl  18353  yonedalem3  18374  yonedainv  18375  plusffn  18745  mulgfval  19198  mulgfvalALT  19199  mulgfn  19201  gimfn  19394  sylow2blem2  19754  rnghmfn  20586  rhmfn  20653  rimfn  20654  rnghmsscmap2  20797  rnghmsscmap  20798  rhmsscmap2  20826  rhmsscmap  20827  srhmsubc  20848  rhmsubclem1  20853  fldc  20956  fldhmsubc  20957  scaffn  21073  lmimfn  21216  ipffn  21870  mplsubrglem  22224  tx1stc  23882  tx2ndc  23883  hmeofn  23989  efmndtmd  24333  qustgplem  24353  nmoffn  24943  rrxmfval  25640  mbfimaopnlem  25889  i1fadd  25929  i1fmul  25930  subsfn  28297  ex-fpar  30950  smatrcl  34314  txomap  34352  qtophaus  34354  pstmxmet  34415  dya2icoseg  34796  dya2iocrfn  34798  fncvm  35844  mpomulnzcnf  36927  cntotbnd  38554  grimfn  48803  grlimfn  48903  rngchomffvalALTV  49201  rngchomrnghmresALTV  49202  rhmsubcALTVlem1  49204  funcringcsetcALTV2lem4  49216  funcringcsetclem4ALTV  49239  srhmsubcALTV  49248  fldcALTV  49255  fldhmsubcALTV  49256  rrx2xpref1o  49656  sectfn  49963  discsubclem  49997  oppffn  50058  swapf2fn  50202  fucofn2  50258  fucoppc  50344  functhinclem1  50378  lanfn  50543  ranfn  50544