Theorem xpexg 7689

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3437   ∪ cun 3896   ⊆ wss 3898  𝒫 cpw 4549   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-opab 5156  df-xp 5625  df-rel 5626

This theorem is referenced by:  xpexd  7690  3xpexg  7691  xpex  7692  sqxpexg  7694  coexg  7865  fex2  7872  fabexgOLD  7875  resfunexgALT  7886  fnexALT  7889  funexw  7890  opabex3d  7903  opabex3rd  7904  opabex3  7905  mpoexxg  8013  fnwelem  8067  naddunif  8614  pmex  8761  mapexOLD  8762  pmvalg  8767  elpmg  8773  fvdiagfn  8821  ixpexg  8852  snmapen  8967  xpdom2  8992  xpdom3  8995  omxpen  8999  fodomr  9048  disjenex  9055  domssex2  9057  domssex  9058  mapxpen  9063  fczfsuppd  9277  brwdom2  9466  xpwdomg  9478  unxpwdom2  9481  djuex  9808  djuexALT  9822  fseqen  9925  djuassen  10077  mapdjuen  10079  djudom1  10081  djuinf  10087  hsmexlem2  10325  axdc2lem  10346  iundom2g  10438  fpwwe2lem12  10540  pwsbas  17393  pwsle  17398  pwssca  17402  isga  19205  efgtf  19636  frgpcpbl  19673  frgp0  19674  frgpeccl  19675  frgpadd  19677  frgpmhm  19679  vrgpf  19682  vrgpinv  19683  frgpupf  19687  frgpup1  19689  frgpup2  19690  frgpup3lem  19691  frgpnabllem1  19787  frgpnabllem2  19788  gsum2d2  19888  gsumcom2  19889  dprd2da  19958  pwssplit3  20997  mpofrlmd  21716  frlmip  21717  mattposvs  22371  mat1dimelbas  22387  mdetrlin  22518  lmfval  23148  txbasex  23482  txopn  23518  txrest  23547  txindislem  23549  xkoinjcn  23603  blfvalps  24299  bcthlem1  25252  bcthlem5  25256  rrxip  25318  isvcOLD  30561  resf1o  32717  locfinref  33875  esum2dlem  34126  esum2d  34127  elsx  34228  satfv0  35423  satf00  35439  filnetlem3  36445  filnetlem4  36446  bj-xpexg2  37025  inxpex  38391  xrninxpex  38461  aks6d1c2  42243  relexpxpnnidm  43820  enrelmap  44114  mpoexxg2  48462  eufsn2  48967