Theorem xpexg 7729

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  𝒫 cpw 4566   × cxp 5639

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  xpexd  7730  3xpexg  7731  xpex  7732  sqxpexg  7734  coexg  7908  fex2  7915  fabexgOLD  7918  resfunexgALT  7929  fnexALT  7932  funexw  7933  opabex3d  7947  opabex3rd  7948  opabex3  7949  mpoexxg  8057  fnwelem  8113  naddunif  8660  pmex  8807  mapexOLD  8808  pmvalg  8813  elpmg  8819  fvdiagfn  8867  ixpexg  8898  snmapen  9012  xpdom2  9041  xpdom3  9044  omxpen  9048  fodomr  9098  disjenex  9105  domssex2  9107  domssex  9108  mapxpen  9113  xpfiOLD  9277  fczfsuppd  9344  brwdom2  9533  xpwdomg  9545  unxpwdom2  9548  djuex  9868  djuexALT  9882  fseqen  9987  djuassen  10139  mapdjuen  10141  djudom1  10143  djuinf  10149  hsmexlem2  10387  axdc2lem  10408  iundom2g  10500  fpwwe2lem12  10602  pwsbas  17457  pwsle  17462  pwssca  17466  isga  19230  efgtf  19659  frgpcpbl  19696  frgp0  19697  frgpeccl  19698  frgpadd  19700  frgpmhm  19702  vrgpf  19705  vrgpinv  19706  frgpupf  19710  frgpup1  19712  frgpup2  19713  frgpup3lem  19714  frgpnabllem1  19810  frgpnabllem2  19811  gsum2d2  19911  gsumcom2  19912  dprd2da  19981  pwssplit3  20975  mpofrlmd  21693  frlmip  21694  mattposvs  22349  mat1dimelbas  22365  mdetrlin  22496  lmfval  23126  txbasex  23460  txopn  23496  txrest  23525  txindislem  23527  xkoinjcn  23581  blfvalps  24278  bcthlem1  25231  bcthlem5  25235  rrxip  25297  isvcOLD  30515  resf1o  32660  locfinref  33838  esum2dlem  34089  esum2d  34090  elsx  34191  satfv0  35352  satf00  35368  filnetlem3  36375  filnetlem4  36376  bj-xpexg2  36955  inxpex  38328  xrninxpex  38387  aks6d1c2  42125  relexpxpnnidm  43699  enrelmap  43993  mpoexxg2  48330  eufsn2  48835