Theorem xpexg 7237

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5480	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7236	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5090	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5090	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5041	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 581	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2106  Vcvv 3397   ∪ cun 3789   ⊆ wss 3791  𝒫 cpw 4378   × cxp 5353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-opab 4949  df-xp 5361  df-rel 5362

This theorem is referenced by:  xpexd  7238  3xpexg  7239  xpex  7240  sqxpexg  7241  coexg  7396  fex2  7400  fabexg  7401  resfunexgALT  7408  fnexALT  7411  opabex3d  7423  opabex3  7424  mpt2exxg  7524  fnwelem  7573  pmex  8145  mapex  8146  pmvalg  8151  elpmg  8156  fvdiagfn  8188  ixpexg  8218  snmapen  8322  xpdom2  8343  xpdom3  8346  omxpen  8350  fodomr  8399  disjenex  8406  domssex2  8408  domssex  8409  mapxpen  8414  xpfi  8519  fczfsuppd  8581  brwdom2  8767  xpwdomg  8779  unxpwdom2  8782  djuex  9068  djuexALT  9081  fseqen  9183  cdaval  9327  cdaassen  9339  mapcdaen  9341  cdadom1  9343  cdainf  9349  hsmexlem2  9584  axdc2lem  9605  iundom2g  9697  fpwwe2lem13  9799  wrdexgOLD  13610  pwsbas  16533  pwsle  16538  pwssca  16542  isga  18107  efgtf  18519  frgpcpbl  18558  frgp0  18559  frgpeccl  18560  frgpadd  18562  frgpmhm  18564  vrgpf  18567  vrgpinv  18568  frgpupf  18572  frgpup1  18574  frgpup2  18575  frgpup3lem  18576  frgpnabllem1  18662  frgpnabllem2  18663  gsum2d2  18759  gsumcom2  18760  dprd2da  18828  pwssplit3  19456  mpt2frlmd  20520  frlmip  20521  mattposvs  20666  mat1dimelbas  20682  mdetrlin  20813  lmfval  21444  txbasex  21778  txopn  21814  txcn  21838  txrest  21843  txindislem  21845  xkoinjcn  21899  blfvalps  22596  bcthlem1  23530  bcthlem5  23534  rrxip  23596  isleag  26196  isvcOLD  28006  resf1o  30071  locfinref  30506  esum2dlem  30752  esum2d  30753  elsx  30855  filnetlem3  32963  filnetlem4  32964  bj-xpexg2  33519  inxpex  34730  xrninxpex  34775  relexpxpnnidm  38945  enrelmap  39240  mpt2exxg2  43124