Theorem fmpo 8114

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 8113	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷)
3		iunxpconst 5731	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
4	3	feq2i 6731	. 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
5	2, 4	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ∀wral 3080  {csn 4588  ∪ ciun 4956   × cxp 5656  ⟶wf 6562   ∈ cmpo 7453

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 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

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 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036

This theorem is used by:  fnmpo  8115  fmpodg  8118  ovmpoelrn  8120  fmpoco  8142  eroprf  8874  uncf  8929  omxpenlem  9135  mapxpen  9200  dffi3  9460  ixpiunwdom  9621  cantnfvalf  9703  iunfictbso  10232  axdc4lem  10572  axcclem  10574  addpqf  11068  mulpqf  11070  subf  11598  xaddf  13394  xmulf  13442  ixxf  13526  ioof  13618  fzf  13683  fzof  13830  axdc4uzlem  14166  sadcf  16667  smupf  16692  gcdf  16728  eucalgf  16802  vdwapf  17194  prdsplusg  17679  prdsmulr  17680  prdsvsca  17681  prdshom  17688  imasvscaf  17761  xpsff1o  17789  wunnat  18184  catcoppccl  18342  catcfuccl  18343  catcxpccl  18431  evlfcl  18446  hofcl  18483  mgmplusf  18876  grpsubf  19279  subgga  19565  lactghmga  19670  sylow1lem2  19864  sylow3lem1  19892  lsmssv  19908  smndlsmidm  19921  efgmf  19978  efgtf  19987  frgpuptf  20035  lmodscaf  21210  xrsds  21768  phlipf  22013  evlslem2  22443  mamucl  22771  matbas2d  22793  mamumat1cl  22809  ordtbas2  23564  iccordt  23587  txuni2  23939  xkotf  23959  txbasval  23980  tx1stc  24024  xkococn  24034  cnmpt12  24041  cnmpt21  24045  cnmpt2t  24047  cnmpt22  24048  cnmptcom  24052  cnmpt2k  24062  txswaphmeo  24179  xpstopnlem1  24183  cnmpt2plusg  24462  cnmpt2vsca  24569  prdsdsf  24741  blfvalps  24757  blfps  24780  blf  24781  stdbdmet  24890  met2ndci  24896  dscmet  24946  xrsxmet  25184  cnmpt2ds  25218  cnmpopc  25304  iimulcn  25314  ishtpy  25348  reparphti  25373  cnmpt2ip  25624  bcthlem5  25704  rrxmet  25784  dyadf  25967  itg1addlem2  26073  mbfi1fseqlem1  26091  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  cxpcn3  27133  sgmf  27529  subsf  28507  midf  29338  grpodivf  31197  nvmf  31304  ipf  31372  hvsubf  31674  ofoprabco  33356  suppovss  33371  elrgspnlem2  33903  fedgmullem1  34372  fedgmullem2  34373  fedgmul  34374  sitmf  35095  cvxsconn  36216  cvmlift2lem5  36280  mblfinlem1  38843  mblfinlem2  38844  sdclem1  38943  metf1o  38955  rrnval  39027  rrnmet  39029  aks6d1c3  43439  fmpocos  43554  resubf  43698  sn-subf  43746  evlselv  43883  frmx  44186  frmy  44187  ofoafg  44617  naddcnff  44625  mnringmulrcld  45487  icof  46505  rescofuf  50539