Theorem fnmpoi 8069

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 8068	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	ax-mp 5	1 ⊢ 𝐹 Fn (𝐴 × 𝐵)

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∀wral 3051  Vcvv 3459   × cxp 5652   Fn wfn 6526   ∈ cmpo 7407

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-oprab 7409  df-mpo 7410  df-1st 7988  df-2nd 7989

This theorem is referenced by:  dmmpo  8070  fnoa  8520  fnom  8521  fnoe  8522  fnmap  8847  fnpm  8848  addpqnq  10952  mulpqnq  10955  mpoaddf  11223  mpomulf  11224  elq  12966  cnref1o  13001  ccatfn  14590  qnnen  16231  restfn  17438  prdsdsfn  17479  imasdsfn  17528  imasvscafn  17551  homffn  17705  comfffn  17716  comffn  17717  isoval  17778  cofucl  17901  fnfuc  17961  natffn  17965  catcisolem  18123  estrchomfn  18147  funcestrcsetclem4  18155  funcsetcestrclem4  18170  fnxpc  18188  1stfcl  18209  2ndfcl  18210  prfcl  18215  evlfcl  18234  curf1cl  18240  curfcl  18244  hofcl  18271  yonedalem3  18292  yonedainv  18293  plusffn  18627  mulgfval  19052  mulgfvalALT  19053  mulgfn  19055  gimfn  19244  sylow2blem2  19602  rnghmfn  20399  rhmfn  20459  rnghmsscmap2  20589  rnghmsscmap  20590  rhmsscmap2  20618  rhmsscmap  20619  srhmsubc  20640  rhmsubclem1  20645  fldc  20744  fldhmsubc  20745  scaffn  20840  lmimfn  20984  ipffn  21611  mplsubrglem  21964  tx1stc  23588  tx2ndc  23589  hmeofn  23695  efmndtmd  24039  qustgplem  24059  nmoffn  24650  rrxmfval  25358  mbfimaopnlem  25608  i1fadd  25648  i1fmul  25649  subsfn  27982  ex-fpar  30443  smatrcl  33827  txomap  33865  qtophaus  33867  pstmxmet  33928  dya2icoseg  34309  dya2iocrfn  34311  fncvm  35279  mpomulnzcnf  36317  cntotbnd  37820  grimfn  47892  grlimfn  47991  rngchomffvalALTV  48253  rngchomrnghmresALTV  48254  rhmsubcALTVlem1  48256  funcringcsetcALTV2lem4  48268  funcringcsetclem4ALTV  48291  srhmsubcALTV  48300  fldcALTV  48307  fldhmsubcALTV  48308  rrx2xpref1o  48698  sectfn  48999  discsubclem  49030  swapf2fn  49185  fucofn2  49235  functhinclem1  49330  lanfn  49486  ranfn  49487