Theorem xpexg 7704

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887   ⊆ wss 3889  𝒫 cpw 4541   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  xpexd  7705  3xpexg  7706  xpex  7707  sqxpexg  7709  coexg  7880  fex2  7887  fabexgOLD  7890  resfunexgALT  7901  fnexALT  7904  funexw  7905  opabex3d  7918  opabex3rd  7919  opabex3  7920  mpoexxg  8028  fnwelem  8081  naddunif  8629  pmex  8778  mapexOLD  8779  pmvalg  8784  elpmg  8790  fvdiagfn  8839  ixpexg  8870  snmapen  8985  xpdom2  9010  xpdom3  9013  omxpen  9017  fodomr  9066  disjenex  9073  domssex2  9075  domssex  9076  mapxpen  9081  fczfsuppd  9299  brwdom2  9488  xpwdomg  9500  unxpwdom2  9503  djuex  9832  djuexALT  9846  fseqen  9949  djuassen  10101  mapdjuen  10103  djudom1  10105  djuinf  10111  hsmexlem2  10349  axdc2lem  10370  iundom2g  10462  fpwwe2lem12  10565  pwsbas  17450  pwsle  17456  pwssca  17460  isga  19266  efgtf  19697  frgpcpbl  19734  frgp0  19735  frgpeccl  19736  frgpadd  19738  frgpmhm  19740  vrgpf  19743  vrgpinv  19744  frgpupf  19748  frgpup1  19750  frgpup2  19751  frgpup3lem  19752  frgpnabllem1  19848  frgpnabllem2  19849  gsum2d2  19949  gsumcom2  19950  dprd2da  20019  pwssplit3  21056  mpofrlmd  21757  frlmip  21758  mattposvs  22420  mat1dimelbas  22436  mdetrlin  22567  lmfval  23197  txbasex  23531  txopn  23567  txrest  23596  txindislem  23598  xkoinjcn  23652  blfvalps  24348  bcthlem1  25291  bcthlem5  25295  rrxip  25357  isvcOLD  30650  resf1o  32803  locfinref  33985  esum2dlem  34236  esum2d  34237  elsx  34338  satfv0  35540  satf00  35556  filnetlem3  36562  filnetlem4  36563  bj-xpexg2  37267  inxpex  38660  xrninxpex  38738  aks6d1c2  42569  relexpxpnnidm  44130  enrelmap  44424  mpoexxg2  48814  eufsn2  49318