Theorem xpexg 7690

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5756	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7683	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5320	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5320	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5265	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903   ⊆ wss 3905  𝒫 cpw 4553   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-opab 5158  df-xp 5629  df-rel 5630

This theorem is referenced by:  xpexd  7691  3xpexg  7692  xpex  7693  sqxpexg  7695  coexg  7869  fex2  7876  fabexgOLD  7879  resfunexgALT  7890  fnexALT  7893  funexw  7894  opabex3d  7907  opabex3rd  7908  opabex3  7909  mpoexxg  8017  fnwelem  8071  naddunif  8618  pmex  8765  mapexOLD  8766  pmvalg  8771  elpmg  8777  fvdiagfn  8825  ixpexg  8856  snmapen  8970  xpdom2  8996  xpdom3  8999  omxpen  9003  fodomr  9052  disjenex  9059  domssex2  9061  domssex  9062  mapxpen  9067  xpfiOLD  9228  fczfsuppd  9295  brwdom2  9484  xpwdomg  9496  unxpwdom2  9499  djuex  9823  djuexALT  9837  fseqen  9940  djuassen  10092  mapdjuen  10094  djudom1  10096  djuinf  10102  hsmexlem2  10340  axdc2lem  10361  iundom2g  10453  fpwwe2lem12  10555  pwsbas  17409  pwsle  17414  pwssca  17418  isga  19188  efgtf  19619  frgpcpbl  19656  frgp0  19657  frgpeccl  19658  frgpadd  19660  frgpmhm  19662  vrgpf  19665  vrgpinv  19666  frgpupf  19670  frgpup1  19672  frgpup2  19673  frgpup3lem  19674  frgpnabllem1  19770  frgpnabllem2  19771  gsum2d2  19871  gsumcom2  19872  dprd2da  19941  pwssplit3  20983  mpofrlmd  21702  frlmip  21703  mattposvs  22358  mat1dimelbas  22374  mdetrlin  22505  lmfval  23135  txbasex  23469  txopn  23505  txrest  23534  txindislem  23536  xkoinjcn  23590  blfvalps  24287  bcthlem1  25240  bcthlem5  25244  rrxip  25306  isvcOLD  30541  resf1o  32686  locfinref  33807  esum2dlem  34058  esum2d  34059  elsx  34160  satfv0  35330  satf00  35346  filnetlem3  36353  filnetlem4  36354  bj-xpexg2  36933  inxpex  38306  xrninxpex  38365  aks6d1c2  42103  relexpxpnnidm  43676  enrelmap  43970  mpoexxg2  48323  eufsn2  48828