Theorem xpexg 7768

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Vcvv 3477   ∪ cun 3960   ⊆ wss 3962  𝒫 cpw 4604   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  xpexd  7769  3xpexg  7770  xpex  7771  sqxpexg  7773  coexg  7951  fex2  7956  fabexgOLD  7959  resfunexgALT  7970  fnexALT  7973  funexw  7974  opabex3d  7988  opabex3rd  7989  opabex3  7990  mpoexxg  8098  fnwelem  8154  naddunif  8729  pmex  8869  mapexOLD  8870  pmvalg  8875  elpmg  8881  fvdiagfn  8929  ixpexg  8960  snmapen  9076  xpdom2  9105  xpdom3  9108  omxpen  9112  fodomr  9166  disjenex  9173  domssex2  9175  domssex  9176  mapxpen  9181  xpfiOLD  9356  fczfsuppd  9423  brwdom2  9610  xpwdomg  9622  unxpwdom2  9625  djuex  9945  djuexALT  9959  fseqen  10064  djuassen  10216  mapdjuen  10218  djudom1  10220  djuinf  10226  hsmexlem2  10464  axdc2lem  10485  iundom2g  10577  fpwwe2lem12  10679  pwsbas  17533  pwsle  17538  pwssca  17542  isga  19321  efgtf  19754  frgpcpbl  19791  frgp0  19792  frgpeccl  19793  frgpadd  19795  frgpmhm  19797  vrgpf  19800  vrgpinv  19801  frgpupf  19805  frgpup1  19807  frgpup2  19808  frgpup3lem  19809  frgpnabllem1  19905  frgpnabllem2  19906  gsum2d2  20006  gsumcom2  20007  dprd2da  20076  pwssplit3  21077  mpofrlmd  21814  frlmip  21815  mattposvs  22476  mat1dimelbas  22492  mdetrlin  22623  lmfval  23255  txbasex  23589  txopn  23625  txrest  23654  txindislem  23656  xkoinjcn  23710  blfvalps  24408  bcthlem1  25371  bcthlem5  25375  rrxip  25437  isvcOLD  30607  resf1o  32747  locfinref  33801  esum2dlem  34072  esum2d  34073  elsx  34174  satfv0  35342  satf00  35358  filnetlem3  36362  filnetlem4  36363  bj-xpexg2  36942  inxpex  38320  xrninxpex  38375  aks6d1c2  42111  relexpxpnnidm  43692  enrelmap  43986  mpoexxg2  48182  eufsn2  48672