Theorem fnmpoi 8056

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   × cxp 5675   Fn wfn 6539   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976

This theorem is referenced by:  dmmpo  8057  fnoa  8508  fnom  8509  fnoe  8510  fnmap  8827  fnpm  8828  addpqnq  10933  mulpqnq  10936  elq  12934  cnref1o  12969  ccatfn  14522  qnnen  16156  restfn  17370  prdsdsfn  17411  imasdsfn  17460  imasvscafn  17483  homffn  17637  comfffn  17648  comffn  17649  isoval  17712  cofucl  17838  fnfuc  17896  natffn  17900  catcisolem  18060  estrchomfn  18086  funcestrcsetclem4  18095  funcsetcestrclem4  18110  fnxpc  18128  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlfcl  18175  curf1cl  18181  curfcl  18185  hofcl  18212  yonedalem3  18233  yonedainv  18234  plusffn  18570  mulgfval  18952  mulgfvalALT  18953  mulgfn  18955  gimfn  19135  sylow2blem2  19489  scaffn  20493  lmimfn  20637  ipffn  21204  mplsubrglem  21563  tx1stc  23154  tx2ndc  23155  hmeofn  23261  efmndtmd  23605  qustgplem  23625  nmoffn  24228  rrxmfval  24923  mbfimaopnlem  25172  i1fadd  25212  i1fmul  25213  subsfn  27502  ex-fpar  29746  smatrcl  32807  txomap  32845  qtophaus  32847  pstmxmet  32908  dya2icoseg  33307  dya2iocrfn  33309  fncvm  34279  mpomulf  35190  mpoaddf  35216  cntotbnd  36712  rnghmfn  46736  rhmfn  46769  rnghmsscmap2  46919  rnghmsscmap  46920  rngchomffvalALTV  46941  rngchomrnghmresALTV  46942  rhmsscmap2  46965  rhmsscmap  46966  funcringcsetcALTV2lem4  46985  funcringcsetclem4ALTV  47008  srhmsubc  47022  fldc  47029  fldhmsubc  47030  rhmsubclem1  47032  srhmsubcALTV  47040  fldcALTV  47047  fldhmsubcALTV  47048  rhmsubcALTVlem1  47050  rrx2xpref1o  47452  functhinclem1  47709