Theorem fnmpoi 8095

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480   × cxp 5683   Fn wfn 6556   ∈ cmpo 7433

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015

This theorem is referenced by:  dmmpo  8096  fnoa  8546  fnom  8547  fnoe  8548  fnmap  8873  fnpm  8874  addpqnq  10978  mulpqnq  10981  mpoaddf  11249  mpomulf  11250  elq  12992  cnref1o  13027  ccatfn  14610  qnnen  16249  restfn  17469  prdsdsfn  17510  imasdsfn  17559  imasvscafn  17582  homffn  17736  comfffn  17747  comffn  17748  isoval  17809  cofucl  17933  fnfuc  17993  natffn  17997  catcisolem  18155  estrchomfn  18179  funcestrcsetclem4  18188  funcsetcestrclem4  18203  fnxpc  18221  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  yonedalem3  18325  yonedainv  18326  plusffn  18662  mulgfval  19087  mulgfvalALT  19088  mulgfn  19090  gimfn  19279  sylow2blem2  19639  rnghmfn  20439  rhmfn  20499  rnghmsscmap2  20629  rnghmsscmap  20630  rhmsscmap2  20658  rhmsscmap  20659  srhmsubc  20680  rhmsubclem1  20685  fldc  20785  fldhmsubc  20786  scaffn  20881  lmimfn  21025  ipffn  21669  mplsubrglem  22024  tx1stc  23658  tx2ndc  23659  hmeofn  23765  efmndtmd  24109  qustgplem  24129  nmoffn  24732  rrxmfval  25440  mbfimaopnlem  25690  i1fadd  25730  i1fmul  25731  subsfn  28056  ex-fpar  30481  smatrcl  33795  txomap  33833  qtophaus  33835  pstmxmet  33896  dya2icoseg  34279  dya2iocrfn  34281  fncvm  35262  mpomulnzcnf  36300  cntotbnd  37803  grimfn  47865  grlimfn  47946  rngchomffvalALTV  48194  rngchomrnghmresALTV  48195  rhmsubcALTVlem1  48197  funcringcsetcALTV2lem4  48209  funcringcsetclem4ALTV  48232  srhmsubcALTV  48241  fldcALTV  48248  fldhmsubcALTV  48249  rrx2xpref1o  48639  swapf2fn  48974  fucofn2  49019  functhinclem1  49093