Theorem fnmpoi 8109

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  ∀wral 3080  Vcvv 3454   × cxp 5654   Fn wfn 6556   ∈ cmpo 7448

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-oprab 7450  df-mpo 7451  df-1st 8028  df-2nd 8029

This theorem is used by:  dmmpo  8110  fnoa  8547  fnom  8548  fnoe  8549  fnmap  8884  fnpm  8885  addpqnq  11053  mulpqnq  11056  mpoaddf  11324  mpomulf  11325  elq  13107  cnref1o  13143  ccatfn  14747  qnnen  16413  restfn  17627  prdsdsfn  17668  imasdsfn  17718  imasvscafn  17741  homffn  17899  comfffn  17910  comffn  17911  isoval  17972  cofucl  18095  fnfuc  18155  natffn  18159  catcisolem  18317  estrchomfn  18341  funcestrcsetclem4  18349  funcsetcestrclem4  18364  fnxpc  18382  1stfcl  18403  2ndfcl  18404  prfcl  18409  evlfcl  18428  curf1cl  18434  curfcl  18438  hofcl  18465  yonedalem3  18486  yonedainv  18487  plusffn  18857  mulgfval  19311  mulgfvalALT  19312  mulgfn  19314  gimfn  19507  sylow2blem2  19868  rnghmfn  20702  rhmfn  20769  rimfn  20770  rnghmsscmap2  20914  rnghmsscmap  20915  rhmsscmap2  20943  rhmsscmap  20944  srhmsubc  20965  rhmsubclem1  20970  fldc  21074  fldhmsubc  21075  scaffn  21191  lmimfn  21334  ipffn  21990  mplsubrglem  22344  tx1stc  24002  tx2ndc  24003  hmeofn  24109  efmndtmd  24453  qustgplem  24473  nmoffn  25063  rrxmfval  25760  mbfimaopnlem  26009  i1fadd  26049  i1fmul  26050  subsfn  28443  ex-fpar  31096  smatrcl  34511  txomap  34549  qtophaus  34551  pstmxmet  34612  dya2icoseg  34992  dya2iocrfn  34994  fncvm  36202  mpomulnzcnf  37279  cntotbnd  38933  grimfn  49192  grlimfn  49292  rngchomffvalALTV  49590  rngchomrnghmresALTV  49591  rhmsubcALTVlem1  49593  funcringcsetcALTV2lem4  49605  funcringcsetclem4ALTV  49628  srhmsubcALTV  49637  fldcALTV  49644  fldhmsubcALTV  49645  fnmpompt  50196  sectfn  50358  discsubclem  50392  oppffn  50455  swapf2fn  50605  fucofn2  50661  fucoppc  50760  functhinclem1  50794  lanfn  51007  ranfn  51008