Theorem xpexg 7700

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5759	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7693	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5314	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5314	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5258	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 593	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888   ⊆ wss 3890  𝒫 cpw 4536   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  xpexd  7701  3xpexg  7702  xpex  7703  sqxpexg  7705  coexg  7876  fex2  7883  fabexgOLD  7886  resfunexgALT  7897  fnexALT  7900  funexw  7901  opabex3d  7914  opabex3rd  7915  opabex3  7916  mpoexxg  8024  fnwelem  8078  naddunif  8626  pmex  8775  mapexOLD  8776  pmvalg  8781  elpmg  8787  fvdiagfn  8836  ixpexg  8867  snmapen  8982  xpdom2  9007  xpdom3  9010  omxpen  9014  fodomr  9063  disjenex  9070  domssex2  9072  domssex  9073  mapxpen  9078  fczfsuppd  9296  brwdom2  9485  xpwdomg  9497  unxpwdom2  9500  djuex  9830  djuexALT  9844  fseqen  9947  djuassen  10099  mapdjuen  10101  djudom1  10103  djuinf  10109  hsmexlem2  10347  axdc2lem  10368  iundom2g  10460  fpwwe2lem12  10563  pwsbas  17448  pwsle  17454  pwssca  17458  isga  19264  efgtf  19695  frgpcpbl  19732  frgp0  19733  frgpeccl  19734  frgpadd  19736  frgpmhm  19738  vrgpf  19741  vrgpinv  19742  frgpupf  19746  frgpup1  19748  frgpup2  19749  frgpup3lem  19750  frgpnabllem1  19846  frgpnabllem2  19847  gsum2d2  19947  gsumcom2  19948  dprd2da  20017  pwssplit3  21058  mpofrlmd  21759  frlmip  21760  mattposvs  22445  mat1dimelbas  22461  mdetrlin  22592  lmfval  23222  txbasex  23556  txopn  23592  txrest  23621  txindislem  23623  xkoinjcn  23677  blfvalps  24373  bcthlem1  25316  bcthlem5  25320  rrxip  25382  isvcOLD  30675  resf1o  32829  locfinref  34032  esum2dlem  34283  esum2d  34284  elsx  34385  satfv0  35593  satf00  35609  filnetlem3  36615  filnetlem4  36616  bj-xpexg2  37320  inxpex  38713  xrninxpex  38791  aks6d1c2  42622  relexpxpnnidm  44154  enrelmap  44448  mpoexxg2  48836  eufsn2  49340