Theorem xpexg 7705

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901   ⊆ wss 3903  𝒫 cpw 4556   × cxp 5630

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 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  xpexd  7706  3xpexg  7707  xpex  7708  sqxpexg  7710  coexg  7881  fex2  7888  fabexgOLD  7891  resfunexgALT  7902  fnexALT  7905  funexw  7906  opabex3d  7919  opabex3rd  7920  opabex3  7921  mpoexxg  8029  fnwelem  8083  naddunif  8631  pmex  8780  mapexOLD  8781  pmvalg  8786  elpmg  8792  fvdiagfn  8841  ixpexg  8872  snmapen  8987  xpdom2  9012  xpdom3  9015  omxpen  9019  fodomr  9068  disjenex  9075  domssex2  9077  domssex  9078  mapxpen  9083  fczfsuppd  9301  brwdom2  9490  xpwdomg  9502  unxpwdom2  9505  djuex  9832  djuexALT  9846  fseqen  9949  djuassen  10101  mapdjuen  10103  djudom1  10105  djuinf  10111  hsmexlem2  10349  axdc2lem  10370  iundom2g  10462  fpwwe2lem12  10565  pwsbas  17419  pwsle  17425  pwssca  17429  isga  19232  efgtf  19663  frgpcpbl  19700  frgp0  19701  frgpeccl  19702  frgpadd  19704  frgpmhm  19706  vrgpf  19709  vrgpinv  19710  frgpupf  19714  frgpup1  19716  frgpup2  19717  frgpup3lem  19718  frgpnabllem1  19814  frgpnabllem2  19815  gsum2d2  19915  gsumcom2  19916  dprd2da  19985  pwssplit3  21025  mpofrlmd  21744  frlmip  21745  mattposvs  22411  mat1dimelbas  22427  mdetrlin  22558  lmfval  23188  txbasex  23522  txopn  23558  txrest  23587  txindislem  23589  xkoinjcn  23643  blfvalps  24339  bcthlem1  25292  bcthlem5  25296  rrxip  25358  isvcOLD  30666  resf1o  32819  locfinref  34018  esum2dlem  34269  esum2d  34270  elsx  34371  satfv0  35571  satf00  35587  filnetlem3  36593  filnetlem4  36594  bj-xpexg2  37202  inxpex  38584  xrninxpex  38662  aks6d1c2  42494  relexpxpnnidm  44053  enrelmap  44347  mpoexxg2  48692  eufsn2  49196