Theorem fnmpoi 8086

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  ∀wral 3051  Vcvv 3462   × cxp 5682   Fn wfn 6551   ∈ cmpo 7428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5306  ax-nul 5313  ax-pr 5435  ax-un 7748

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-iun 5005  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-fv 6564  df-oprab 7430  df-mpo 7431  df-1st 8005  df-2nd 8006

This theorem is referenced by:  dmmpo  8087  fnoa  8540  fnom  8541  fnoe  8542  fnmap  8864  fnpm  8865  addpqnq  10983  mulpqnq  10986  mpoaddf  11254  mpomulf  11255  elq  12988  cnref1o  13023  ccatfn  14582  qnnen  16217  restfn  17441  prdsdsfn  17482  imasdsfn  17531  imasvscafn  17554  homffn  17708  comfffn  17719  comffn  17720  isoval  17783  cofucl  17909  fnfuc  17970  natffn  17974  catcisolem  18134  estrchomfn  18160  funcestrcsetclem4  18169  funcsetcestrclem4  18184  fnxpc  18202  1stfcl  18223  2ndfcl  18224  prfcl  18229  evlfcl  18249  curf1cl  18255  curfcl  18259  hofcl  18286  yonedalem3  18307  yonedainv  18308  plusffn  18644  mulgfval  19065  mulgfvalALT  19066  mulgfn  19068  gimfn  19257  sylow2blem2  19621  rnghmfn  20423  rhmfn  20483  rnghmsscmap2  20609  rnghmsscmap  20610  rhmsscmap2  20638  rhmsscmap  20639  srhmsubc  20660  rhmsubclem1  20665  fldc  20765  fldhmsubc  20766  scaffn  20861  lmimfn  21006  ipffn  21649  mplsubrglem  22015  tx1stc  23648  tx2ndc  23649  hmeofn  23755  efmndtmd  24099  qustgplem  24119  nmoffn  24722  rrxmfval  25428  mbfimaopnlem  25678  i1fadd  25718  i1fmul  25719  subsfn  28037  ex-fpar  30398  smatrcl  33613  txomap  33651  qtophaus  33653  pstmxmet  33714  dya2icoseg  34113  dya2iocrfn  34115  fncvm  35087  mpomulnzcnf  36013  cntotbnd  37499  grimfn  47462  grlimfn  47503  rngchomffvalALTV  47673  rngchomrnghmresALTV  47674  rhmsubcALTVlem1  47676  funcringcsetcALTV2lem4  47688  funcringcsetclem4ALTV  47711  srhmsubcALTV  47720  fldcALTV  47727  fldhmsubcALTV  47728  rrx2xpref1o  48124  functhinclem1  48380