Theorem xpexg 7753

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5787	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7749	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5340	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5340	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 19	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5281	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 599	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897   ⊆ wss 3899  𝒫 cpw 4557   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  xpexd  7754  3xpexg  7755  xpex  7756  sqxpexg  7758  coexg  7930  fex2  7937  resfunexgALT  7949  fnexALT  7952  funexw  7953  opabex3d  7966  opabex3rd  7967  opabex3  7968  mpoexxg  8077  fnwelem  8132  naddunif  8687  pmex  8836  pmvalg  8841  elpmg  8847  fvdiagfn  8903  ixpexg  8934  snmapen  9050  xpdom2  9075  xpdom3  9078  omxpen  9082  fodomr  9131  disjenex  9138  domssex2  9140  domssex  9141  mapxpen  9146  fczfsuppd  9362  brwdom2  9551  xpwdomg  9563  unxpwdom2  9566  djuex  9970  djuexALT  9984  fseqen  10087  djuassen  10238  mapdjuen  10240  djudom1  10242  djuinf  10248  hsmexlem2  10486  axdc2lem  10507  iundom2g  10605  fpwwe2lem12  10708  pwsbas  17638  pwsle  17644  pwssca  17648  isga  19485  efgtf  19916  frgpcpbl  19953  frgp0  19954  frgpeccl  19955  frgpadd  19957  frgpmhm  19959  vrgpf  19962  vrgpinv  19963  frgpupf  19967  frgpup1  19969  frgpup2  19970  frgpup3lem  19971  frgpnabllem1  20067  frgpnabllem2  20068  gsum2d2  20168  gsumcom2  20169  dprd2da  20238  pwssplit3  21316  mpofrlmd  22063  frlmip  22064  mattposvs  22750  mat1dimelbas  22766  mdetrlin  22897  lmfval  23530  txbasex  23865  txopn  23901  txrest  23930  txindislem  23932  xkoinjcn  23986  blfvalps  24682  bcthlem1  25625  bcthlem5  25629  rrxip  25691  isvcOLD  31163  resf1o  33304  locfinref  34455  esum2dlem  34706  esum2d  34707  elsx  34809  satfv0  36092  satf00  36108  filnetlem3  37138  filnetlem4  37139  bj-xpexg2  37843  inxpex  39239  xrninxpex  39317  aks6d1c2  43148  relexpxpnnidm  44662  enrelmap  44956  mpoexxg2  49394  eufsn2  49897