Theorem xpexg 7764

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

Assertion

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

Proof of Theorem xpexg

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   ∪ cun 4149  𝒫 cpw 4556   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  xpexd  7765  3xpexg  7766  xpex  7767  sqxpexg  7769  coexg  7941  fex2  7948  resfunexgALT  7960  fnexALT  7963  funexw  7964  opabex3d  7977  opabex3rd  7978  opabex3  7979  mpoexxg  8088  fnwelem  8143  naddunif  8704  pmex  8853  pmvalg  8858  elpmg  8864  fvdiagfn  8920  ixpexg  8951  snmapen  9067  xpdom2  9092  xpdom3  9095  omxpen  9099  fodomr  9148  disjenex  9155  domssex2  9157  domssex  9158  mapxpen  9163  fczfsuppd  9379  brwdom2  9568  xpwdomg  9580  unxpwdom2  9583  djuex  9990  djuexALT  10004  fseqen  10107  djuassen  10258  mapdjuen  10260  djudom1  10262  djuinf  10268  hsmexlem2  10506  axdc2lem  10527  iundom2g  10625  fpwwe2lem12  10728  pwsbas  17659  pwsle  17665  pwssca  17669  isga  19506  efgtf  19937  frgpcpbl  19974  frgp0  19975  frgpeccl  19976  frgpadd  19978  frgpmhm  19980  vrgpf  19983  vrgpinv  19984  frgpupf  19988  frgpup1  19990  frgpup2  19991  frgpup3lem  19992  frgpnabllem1  20088  frgpnabllem2  20089  gsum2d2  20189  gsumcom2  20190  dprd2da  20259  pwssplit3  21337  mpofrlmd  22084  frlmip  22085  mattposvs  22771  mat1dimelbas  22787  mdetrlin  22918  lmfval  23551  txbasex  23886  txopn  23922  txrest  23951  txindislem  23953  xkoinjcn  24007  blfvalps  24703  bcthlem1  25646  bcthlem5  25650  rrxip  25712  isvcOLD  31182  resf1o  33365  locfinref  34516  esum2dlem  34767  esum2d  34768  elsx  34870  satfv0  36192  satf00  36208  filnetlem3  37243  filnetlem4  37244  bj-xpexg2  37948  inxpex  39347  xrninxpex  39425  aks6d1c2  43256  relexpxpnnidm  44779  enrelmap  45073  mpoexxg2  49526  eufsn2  50029