Theorem xpexg 7737

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5786	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7730	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5339	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5339	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 19	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5283	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 598	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905   ⊆ wss 3907  𝒫 cpw 4558   × cxp 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-opab 5167  df-xp 5657  df-rel 5658

This theorem is referenced by:  xpexd  7738  3xpexg  7739  xpex  7740  sqxpexg  7742  coexg  7914  fex2  7921  resfunexgALT  7933  fnexALT  7936  funexw  7937  opabex3d  7950  opabex3rd  7951  opabex3  7952  mpoexxg  8060  fnwelem  8115  naddunif  8668  pmex  8817  pmvalg  8822  elpmg  8828  fvdiagfn  8877  ixpexg  8908  snmapen  9023  xpdom2  9048  xpdom3  9051  omxpen  9055  fodomr  9104  disjenex  9111  domssex2  9113  domssex  9114  mapxpen  9119  fczfsuppd  9334  brwdom2  9523  xpwdomg  9535  unxpwdom2  9538  djuex  9882  djuexALT  9896  fseqen  9999  djuassen  10150  mapdjuen  10152  djudom1  10154  djuinf  10160  hsmexlem2  10399  axdc2lem  10420  iundom2g  10512  fpwwe2lem12  10615  pwsbas  17528  pwsle  17534  pwssca  17538  isga  19349  efgtf  19780  frgpcpbl  19817  frgp0  19818  frgpeccl  19819  frgpadd  19821  frgpmhm  19823  vrgpf  19826  vrgpinv  19827  frgpupf  19831  frgpup1  19833  frgpup2  19834  frgpup3lem  19835  frgpnabllem1  19931  frgpnabllem2  19932  gsum2d2  20032  gsumcom2  20033  dprd2da  20102  pwssplit3  21148  mpofrlmd  21884  frlmip  21885  mattposvs  22569  mat1dimelbas  22585  mdetrlin  22716  lmfval  23346  txbasex  23680  txopn  23716  txrest  23745  txindislem  23747  xkoinjcn  23801  blfvalps  24497  bcthlem1  25440  bcthlem5  25444  rrxip  25506  isvcOLD  30836  resf1o  32983  locfinref  34143  esum2dlem  34394  esum2d  34395  elsx  34496  satfv0  35716  satf00  35732  filnetlem3  36748  filnetlem4  36749  bj-xpexg2  37452  inxpex  38845  xrninxpex  38923  aks6d1c2  42754  relexpxpnnidm  44286  enrelmap  44580  mpoexxg2  48970  eufsn2  49473