Theorem xpexg 7770

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949   ⊆ wss 3951  𝒫 cpw 4600   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  xpexd  7771  3xpexg  7772  xpex  7773  sqxpexg  7775  coexg  7951  fex2  7958  fabexgOLD  7961  resfunexgALT  7972  fnexALT  7975  funexw  7976  opabex3d  7990  opabex3rd  7991  opabex3  7992  mpoexxg  8100  fnwelem  8156  naddunif  8731  pmex  8871  mapexOLD  8872  pmvalg  8877  elpmg  8883  fvdiagfn  8931  ixpexg  8962  snmapen  9078  xpdom2  9107  xpdom3  9110  omxpen  9114  fodomr  9168  disjenex  9175  domssex2  9177  domssex  9178  mapxpen  9183  xpfiOLD  9359  fczfsuppd  9426  brwdom2  9613  xpwdomg  9625  unxpwdom2  9628  djuex  9948  djuexALT  9962  fseqen  10067  djuassen  10219  mapdjuen  10221  djudom1  10223  djuinf  10229  hsmexlem2  10467  axdc2lem  10488  iundom2g  10580  fpwwe2lem12  10682  pwsbas  17532  pwsle  17537  pwssca  17541  isga  19309  efgtf  19740  frgpcpbl  19777  frgp0  19778  frgpeccl  19779  frgpadd  19781  frgpmhm  19783  vrgpf  19786  vrgpinv  19787  frgpupf  19791  frgpup1  19793  frgpup2  19794  frgpup3lem  19795  frgpnabllem1  19891  frgpnabllem2  19892  gsum2d2  19992  gsumcom2  19993  dprd2da  20062  pwssplit3  21060  mpofrlmd  21797  frlmip  21798  mattposvs  22461  mat1dimelbas  22477  mdetrlin  22608  lmfval  23240  txbasex  23574  txopn  23610  txrest  23639  txindislem  23641  xkoinjcn  23695  blfvalps  24393  bcthlem1  25358  bcthlem5  25362  rrxip  25424  isvcOLD  30598  resf1o  32741  locfinref  33840  esum2dlem  34093  esum2d  34094  elsx  34195  satfv0  35363  satf00  35379  filnetlem3  36381  filnetlem4  36382  bj-xpexg2  36961  inxpex  38340  xrninxpex  38395  aks6d1c2  42131  relexpxpnnidm  43716  enrelmap  44010  mpoexxg2  48254  eufsn2  48752