Theorem xpexg 7758

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

Assertion

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

Proof of Theorem xpexg

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906   ⊆ wss 3908  𝒫 cpw 4567   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  xpexd  7759  3xpexg  7760  xpex  7761  sqxpexg  7763  coexg  7935  fex2  7942  resfunexgALT  7954  fnexALT  7957  funexw  7958  opabex3d  7971  opabex3rd  7972  opabex3  7973  mpoexxg  8081  fnwelem  8136  naddunif  8689  pmex  8838  pmvalg  8843  elpmg  8849  fvdiagfn  8898  ixpexg  8929  snmapen  9045  xpdom2  9070  xpdom3  9073  omxpen  9077  fodomr  9126  disjenex  9133  domssex2  9135  domssex  9136  mapxpen  9141  fczfsuppd  9356  brwdom2  9545  xpwdomg  9557  unxpwdom2  9560  djuex  9913  djuexALT  9927  fseqen  10030  djuassen  10181  mapdjuen  10183  djudom1  10185  djuinf  10191  hsmexlem2  10429  axdc2lem  10450  iundom2g  10542  fpwwe2lem12  10645  pwsbas  17565  pwsle  17571  pwssca  17575  isga  19392  efgtf  19823  frgpcpbl  19860  frgp0  19861  frgpeccl  19862  frgpadd  19864  frgpmhm  19866  vrgpf  19869  vrgpinv  19870  frgpupf  19874  frgpup1  19876  frgpup2  19877  frgpup3lem  19878  frgpnabllem1  19974  frgpnabllem2  19975  gsum2d2  20075  gsumcom2  20076  dprd2da  20145  pwssplit3  21219  mpofrlmd  21964  frlmip  21965  mattposvs  22649  mat1dimelbas  22665  mdetrlin  22796  lmfval  23426  txbasex  23760  txopn  23796  txrest  23825  txindislem  23827  xkoinjcn  23881  blfvalps  24577  bcthlem1  25520  bcthlem5  25524  rrxip  25586  isvcOLD  30968  resf1o  33112  locfinref  34262  esum2dlem  34513  esum2d  34514  elsx  34616  satfv0  35871  satf00  35887  filnetlem3  36932  filnetlem4  36933  bj-xpexg2  37637  inxpex  39029  xrninxpex  39107  aks6d1c2  42938  relexpxpnnidm  44470  enrelmap  44764  mpoexxg2  49159  eufsn2  49662