Theorem xpexg 7683

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Vcvv 3436   ∪ cun 3900   ⊆ wss 3902  𝒫 cpw 4550   × cxp 5614

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  xpexd  7684  3xpexg  7685  xpex  7686  sqxpexg  7688  coexg  7859  fex2  7866  fabexgOLD  7869  resfunexgALT  7880  fnexALT  7883  funexw  7884  opabex3d  7897  opabex3rd  7898  opabex3  7899  mpoexxg  8007  fnwelem  8061  naddunif  8608  pmex  8755  mapexOLD  8756  pmvalg  8761  elpmg  8767  fvdiagfn  8815  ixpexg  8846  snmapen  8960  xpdom2  8985  xpdom3  8988  omxpen  8992  fodomr  9041  disjenex  9048  domssex2  9050  domssex  9051  mapxpen  9056  fczfsuppd  9270  brwdom2  9459  xpwdomg  9471  unxpwdom2  9474  djuex  9798  djuexALT  9812  fseqen  9915  djuassen  10067  mapdjuen  10069  djudom1  10071  djuinf  10077  hsmexlem2  10315  axdc2lem  10336  iundom2g  10428  fpwwe2lem12  10530  pwsbas  17388  pwsle  17393  pwssca  17397  isga  19201  efgtf  19632  frgpcpbl  19669  frgp0  19670  frgpeccl  19671  frgpadd  19673  frgpmhm  19675  vrgpf  19678  vrgpinv  19679  frgpupf  19683  frgpup1  19685  frgpup2  19686  frgpup3lem  19687  frgpnabllem1  19783  frgpnabllem2  19784  gsum2d2  19884  gsumcom2  19885  dprd2da  19954  pwssplit3  20993  mpofrlmd  21712  frlmip  21713  mattposvs  22368  mat1dimelbas  22384  mdetrlin  22515  lmfval  23145  txbasex  23479  txopn  23515  txrest  23544  txindislem  23546  xkoinjcn  23600  blfvalps  24296  bcthlem1  25249  bcthlem5  25253  rrxip  25315  isvcOLD  30554  resf1o  32708  locfinref  33849  esum2dlem  34100  esum2d  34101  elsx  34202  satfv0  35390  satf00  35406  filnetlem3  36413  filnetlem4  36414  bj-xpexg2  36993  inxpex  38366  xrninxpex  38425  aks6d1c2  42162  relexpxpnnidm  43735  enrelmap  44029  mpoexxg2  48368  eufsn2  48873