Theorem fmpo 8077

Description: Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)

Hypothesis

Ref	Expression
fmpo.1	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Assertion

Ref	Expression
fmpo	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐷,𝑦

Allowed substitution hints:   𝐶(𝑥, 𝑦)   𝐹(𝑥, 𝑦)

Proof of Theorem fmpo

Step	Hyp	Ref	Expression
1		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
2	1	fmpox 8076	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷)
3		iunxpconst 5724	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
4	3	feq2i 6699	. 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
5	2, 4	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3077  {csn 4584  ∪ ciun 4951   × cxp 5649  ⟶wf 6533   ∈ cmpo 7420

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000

This theorem is used by:  fnmpo  8078  fmpodg  8081  ovmpoelrn  8083  fmpoco  8104  eroprf  8829  uncf  8884  omxpenlem  9090  mapxpen  9155  dffi3  9416  ixpiunwdom  9577  cantnfvalf  9659  iunfictbso  10186  axdc4lem  10526  axcclem  10528  addpqf  11022  mulpqf  11024  subf  11552  xaddf  13347  xmulf  13395  ixxf  13479  ioof  13571  fzf  13636  fzof  13783  axdc4uzlem  14119  sadcf  16616  smupf  16641  gcdf  16677  eucalgf  16751  vdwapf  17143  prdsplusg  17622  prdsmulr  17623  prdsvsca  17624  prdshom  17631  imasvscaf  17704  xpsff1o  17732  wunnat  18127  catcoppccl  18285  catcfuccl  18286  catcxpccl  18374  evlfcl  18389  hofcl  18426  mgmplusf  18819  grpsubf  19222  subgga  19507  lactghmga  19612  sylow1lem2  19806  sylow3lem1  19834  lsmssv  19850  smndlsmidm  19863  efgmf  19920  efgtf  19929  frgpuptf  19977  lmodscaf  21152  xrsds  21709  phlipf  21951  evlslem2  22381  mamucl  22709  matbas2d  22731  mamumat1cl  22747  ordtbas2  23502  iccordt  23525  txuni2  23877  xkotf  23897  txbasval  23918  tx1stc  23962  xkococn  23972  cnmpt12  23979  cnmpt21  23983  cnmpt2t  23985  cnmpt22  23986  cnmptcom  23990  cnmpt2k  24000  txswaphmeo  24117  xpstopnlem1  24121  cnmpt2plusg  24400  cnmpt2vsca  24507  prdsdsf  24679  blfvalps  24695  blfps  24718  blf  24719  stdbdmet  24828  met2ndci  24834  dscmet  24884  xrsxmet  25122  cnmpt2ds  25156  cnmpopc  25242  iimulcn  25252  ishtpy  25286  reparphti  25311  cnmpt2ip  25562  bcthlem5  25642  rrxmet  25722  dyadf  25905  itg1addlem2  26011  mbfi1fseqlem1  26029  mbfi1fseqlem3  26031  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  cxpcn3  27069  sgmf  27465  subsf  28443  midf  29274  grpodivf  31133  nvmf  31240  ipf  31308  hvsubf  31610  ofoprabco  33251  suppovss  33267  elrgspnlem2  33797  fedgmullem1  34254  fedgmullem2  34255  fedgmul  34256  sitmf  34977  cvxsconn  35987  cvmlift2lem5  36051  mblfinlem1  38555  mblfinlem2  38556  sdclem1  38657  metf1o  38669  rrnval  38741  rrnmet  38743  aks6d1c3  43153  fmpocos  43267  resubf  43412  sn-subf  43460  evlselv  43597  frmx  43899  frmy  43900  ofoafg  44340  naddcnff  44348  mnringmulrcld  45211  icof  46201  rescofuf  50170