Theorem xpexg 6835

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5145	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 6834	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 4771	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 4771	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 4727	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 693	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 1976  Vcvv 3172   ∪ cun 3537   ⊆ wss 3539  𝒫 cpw 4107   × cxp 5026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-opab 4638  df-xp 5034  df-rel 5035

This theorem is referenced by:  3xpexg  6836  xpex  6837  sqxpexg  6838  opabex2  6974  cnvexg  6982  coexg  6987  fex2  6991  fabexg  6992  resfunexgALT  6999  cofunexg  7000  fnexALT  7002  opabex3d  7014  opabex3  7015  oprabexd  7023  ofmresex  7033  mpt2exxg  7110  offval22  7117  fnwelem  7156  tposexg  7230  pmex  7726  mapex  7727  pmvalg  7732  elpmg  7736  fvdiagfn  7765  ixpexg  7795  map1  7898  xpdom2  7917  xpdom3  7920  omxpen  7924  fodomr  7973  disjenex  7980  domssex2  7982  domssex  7983  mapxpen  7988  xpfi  8093  fczfsuppd  8153  marypha1  8200  brwdom2  8338  wdom2d  8345  xpwdomg  8350  unxpwdom2  8353  ixpiunwdom  8356  fseqen  8710  cdaval  8852  cdaassen  8864  mapcdaen  8866  cdadom1  8868  cdainf  8874  hsmexlem2  9109  axdc2lem  9130  iundom2g  9218  fpwwe2lem2  9310  fpwwe2lem5  9312  fpwwe2lem12  9319  fpwwe2lem13  9320  fpwwelem  9323  canthwe  9329  pwxpndom  9344  gchhar  9357  wrdexg  13116  trclexlem  13527  pwsbas  15916  pwsle  15921  pwssca  15925  isacs1i  16087  rescval2  16257  reschom  16259  rescabs  16262  setccofval  16501  isga  17493  sylow2a  17803  lsmhash  17887  efgtf  17904  frgpcpbl  17941  frgp0  17942  frgpeccl  17943  frgpadd  17945  frgpmhm  17947  vrgpf  17950  vrgpinv  17951  frgpupf  17955  frgpup1  17957  frgpup2  17958  frgpup3lem  17959  frgpnabllem1  18045  frgpnabllem2  18046  gsum2d2  18142  gsumcom2  18143  gsumxp  18144  dprd2da  18210  pwssplit3  18828  opsrval  19241  opsrtoslem2  19252  evlslem4  19275  mpt2frlmd  19877  frlmip  19878  matbas2d  19990  mattposvs  20022  mat1dimelbas  20038  mdetrlin  20169  lmfval  20788  txbasex  21121  txopn  21157  txcn  21181  txrest  21186  txindislem  21188  xkoinjcn  21242  tsmsxp  21710  ustssel  21761  ustfilxp  21768  trust  21785  restutop  21793  trcfilu  21850  cfiluweak  21851  imasdsf1olem  21929  blfvalps  21939  metustfbas  22113  restmetu  22126  bcthlem1  22846  bcthlem5  22850  rrxip  22903  perpln1  25323  perpln2  25324  isperp  25325  isleag  25451  isvcOLD  26602  fnct  28682  resf1o  28699  locfinref  29042  metidval  29067  esum2dlem  29287  esum2d  29288  esumiun  29289  elsx  29390  filnetlem3  31351  filnetlem4  31352  bj-xpexg2  31936  isrngod  32663  isgrpda  32720  iscringd  32763  wdom2d2  36416  unxpwdom3  36479  trclubgNEW  36740  relexpxpnnidm  36810  relexpxpmin  36824  enrelmap  37107  rfovd  37111  rfovcnvf1od  37114  fsovrfovd  37119  xpexd  38110  dvsinax  38598  sge0xp  39119  mpt2exxg2  41904