Theorem xpexg 7744

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924   ⊆ wss 3926  𝒫 cpw 4575   × cxp 5652

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  xpexd  7745  3xpexg  7746  xpex  7747  sqxpexg  7749  coexg  7925  fex2  7932  fabexgOLD  7935  resfunexgALT  7946  fnexALT  7949  funexw  7950  opabex3d  7964  opabex3rd  7965  opabex3  7966  mpoexxg  8074  fnwelem  8130  naddunif  8705  pmex  8845  mapexOLD  8846  pmvalg  8851  elpmg  8857  fvdiagfn  8905  ixpexg  8936  snmapen  9052  xpdom2  9081  xpdom3  9084  omxpen  9088  fodomr  9142  disjenex  9149  domssex2  9151  domssex  9152  mapxpen  9157  xpfiOLD  9331  fczfsuppd  9398  brwdom2  9587  xpwdomg  9599  unxpwdom2  9602  djuex  9922  djuexALT  9936  fseqen  10041  djuassen  10193  mapdjuen  10195  djudom1  10197  djuinf  10203  hsmexlem2  10441  axdc2lem  10462  iundom2g  10554  fpwwe2lem12  10656  pwsbas  17501  pwsle  17506  pwssca  17510  isga  19274  efgtf  19703  frgpcpbl  19740  frgp0  19741  frgpeccl  19742  frgpadd  19744  frgpmhm  19746  vrgpf  19749  vrgpinv  19750  frgpupf  19754  frgpup1  19756  frgpup2  19757  frgpup3lem  19758  frgpnabllem1  19854  frgpnabllem2  19855  gsum2d2  19955  gsumcom2  19956  dprd2da  20025  pwssplit3  21019  mpofrlmd  21737  frlmip  21738  mattposvs  22393  mat1dimelbas  22409  mdetrlin  22540  lmfval  23170  txbasex  23504  txopn  23540  txrest  23569  txindislem  23571  xkoinjcn  23625  blfvalps  24322  bcthlem1  25276  bcthlem5  25280  rrxip  25342  isvcOLD  30560  resf1o  32707  locfinref  33872  esum2dlem  34123  esum2d  34124  elsx  34225  satfv0  35380  satf00  35396  filnetlem3  36398  filnetlem4  36399  bj-xpexg2  36978  inxpex  38357  xrninxpex  38412  aks6d1c2  42143  relexpxpnnidm  43727  enrelmap  44021  mpoexxg2  48313  eufsn2  48821