Theorem xpexg 7578

Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7797. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
xpexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5708	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7577	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5296	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5296	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5242	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 586	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881   ⊆ wss 3883  𝒫 cpw 4530   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-opab 5133  df-xp 5586  df-rel 5587

This theorem is referenced by:  xpexd  7579  3xpexg  7580  xpex  7581  sqxpexg  7583  coexg  7750  fex2  7754  fabexg  7755  resfunexgALT  7764  fnexALT  7767  funexw  7768  opabex3d  7781  opabex3rd  7782  opabex3  7783  mpoexxg  7889  fnwelem  7943  pmex  8578  mapex  8579  pmvalg  8584  elpmg  8589  fvdiagfn  8637  ixpexg  8668  snmapen  8782  xpdom2  8807  xpdom3  8810  omxpen  8814  fodomr  8864  disjenex  8871  domssex2  8873  domssex  8874  mapxpen  8879  xpfi  9015  fczfsuppd  9076  brwdom2  9262  xpwdomg  9274  unxpwdom2  9277  djuex  9597  djuexALT  9611  fseqen  9714  djuassen  9865  mapdjuen  9867  djudom1  9869  djuinf  9875  hsmexlem2  10114  axdc2lem  10135  iundom2g  10227  fpwwe2lem12  10329  pwsbas  17115  pwsle  17120  pwssca  17124  isga  18812  efgtf  19243  frgpcpbl  19280  frgp0  19281  frgpeccl  19282  frgpadd  19284  frgpmhm  19286  vrgpf  19289  vrgpinv  19290  frgpupf  19294  frgpup1  19296  frgpup2  19297  frgpup3lem  19298  frgpnabllem1  19389  frgpnabllem2  19390  gsum2d2  19490  gsumcom2  19491  dprd2da  19560  pwssplit3  20238  mpofrlmd  20894  frlmip  20895  mattposvs  21512  mat1dimelbas  21528  mdetrlin  21659  lmfval  22291  txbasex  22625  txopn  22661  txrest  22690  txindislem  22692  xkoinjcn  22746  blfvalps  23444  bcthlem1  24393  bcthlem5  24397  rrxip  24459  isvcOLD  28842  resf1o  30967  locfinref  31693  esum2dlem  31960  esum2d  31961  elsx  32062  satfv0  33220  satf00  33236  filnetlem3  34496  filnetlem4  34497  bj-xpexg2  35077  inxpex  36401  xrninxpex  36447  relexpxpnnidm  41200  enrelmap  41494  mpoexxg2  45561  eufsn2  46058