Theorem xpexg 7765

Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7994. (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 7761	. . 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 7752

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 4585  df-pr 4587  df-op 4835  df-uni 4867  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  xpexd  7766  3xpexg  7767  xpex  7768  sqxpexg  7770  coexg  7942  fex2  7949  resfunexgALT  7961  fnexALT  7964  funexw  7965  opabex3d  7978  opabex3rd  7979  opabex3  7980  mpoexxg  8089  fnwelem  8146  naddunif  8707  pmex  8856  pmvalg  8861  elpmg  8867  fvdiagfn  8923  ixpexg  8954  snmapen  9070  xpdom2  9095  xpdom3  9098  omxpen  9102  fodomr  9151  disjenex  9158  domssex2  9160  domssex  9161  mapxpen  9166  fczfsuppd  9382  brwdom2  9571  xpwdomg  9583  unxpwdom2  9586  djuex  9993  djuexALT  10007  fseqen  10110  djuassen  10261  mapdjuen  10263  djudom1  10265  djuinf  10271  hsmexlem2  10509  axdc2lem  10530  iundom2g  10628  fpwwe2lem12  10731  pwsbas  17664  pwsle  17670  pwssca  17674  isga  19511  efgtf  19942  frgpcpbl  19979  frgp0  19980  frgpeccl  19981  frgpadd  19983  frgpmhm  19985  vrgpf  19988  vrgpinv  19989  frgpupf  19993  frgpup1  19995  frgpup2  19996  frgpup3lem  19997  frgpnabllem1  20093  frgpnabllem2  20094  gsum2d2  20194  gsumcom2  20195  dprd2da  20264  pwssplit3  21342  mpofrlmd  22089  frlmip  22090  mattposvs  22776  mat1dimelbas  22792  mdetrlin  22923  lmfval  23556  txbasex  23891  txopn  23927  txrest  23956  txindislem  23958  xkoinjcn  24012  blfvalps  24708  bcthlem1  25651  bcthlem5  25655  rrxip  25717  isvcOLD  31187  resf1o  33369  locfinref  34520  esum2dlem  34771  esum2d  34772  elsx  34874  satfv0  36210  satf00  36226  filnetlem3  37261  filnetlem4  37262  bj-xpexg2  37966  inxpex  39365  xrninxpex  39443  aks6d1c2  43274  relexpxpnnidm  44797  enrelmap  45091  mpoexxg2  49544  eufsn2  50048