Theorem xpexg 7697

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5758	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7690	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5315	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5315	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5260	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 588	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  𝒫 cpw 4542   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-opab 5149  df-xp 5630  df-rel 5631

This theorem is referenced by:  xpexd  7698  3xpexg  7699  xpex  7700  sqxpexg  7702  coexg  7873  fex2  7880  fabexgOLD  7883  resfunexgALT  7894  fnexALT  7897  funexw  7898  opabex3d  7911  opabex3rd  7912  opabex3  7913  mpoexxg  8021  fnwelem  8074  naddunif  8622  pmex  8771  mapexOLD  8772  pmvalg  8777  elpmg  8783  fvdiagfn  8832  ixpexg  8863  snmapen  8978  xpdom2  9003  xpdom3  9006  omxpen  9010  fodomr  9059  disjenex  9066  domssex2  9068  domssex  9069  mapxpen  9074  fczfsuppd  9292  brwdom2  9481  xpwdomg  9493  unxpwdom2  9496  djuex  9823  djuexALT  9837  fseqen  9940  djuassen  10092  mapdjuen  10094  djudom1  10096  djuinf  10102  hsmexlem2  10340  axdc2lem  10361  iundom2g  10453  fpwwe2lem12  10556  pwsbas  17441  pwsle  17447  pwssca  17451  isga  19257  efgtf  19688  frgpcpbl  19725  frgp0  19726  frgpeccl  19727  frgpadd  19729  frgpmhm  19731  vrgpf  19734  vrgpinv  19735  frgpupf  19739  frgpup1  19741  frgpup2  19742  frgpup3lem  19743  frgpnabllem1  19839  frgpnabllem2  19840  gsum2d2  19940  gsumcom2  19941  dprd2da  20010  pwssplit3  21048  mpofrlmd  21767  frlmip  21768  mattposvs  22430  mat1dimelbas  22446  mdetrlin  22577  lmfval  23207  txbasex  23541  txopn  23577  txrest  23606  txindislem  23608  xkoinjcn  23662  blfvalps  24358  bcthlem1  25301  bcthlem5  25305  rrxip  25367  isvcOLD  30665  resf1o  32818  locfinref  34001  esum2dlem  34252  esum2d  34253  elsx  34354  satfv0  35556  satf00  35572  filnetlem3  36578  filnetlem4  36579  bj-xpexg2  37283  inxpex  38674  xrninxpex  38752  aks6d1c2  42583  relexpxpnnidm  44148  enrelmap  44442  mpoexxg2  48826  eufsn2  49330