Theorem xpexg 7190

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5434	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7189	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5048	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5048	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 4999	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 577	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2156  Vcvv 3391   ∪ cun 3767   ⊆ wss 3769  𝒫 cpw 4351   × cxp 5309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-opab 4907  df-xp 5317  df-rel 5318

This theorem is referenced by:  3xpexg  7191  xpex  7192  sqxpexg  7193  cnvexg  7342  coexg  7347  fex2  7351  fabexg  7352  resfunexgALT  7359  cofunexg  7360  fnexALT  7362  opabex3d  7375  opabex3  7376  oprabexd  7385  ofmresex  7395  opabex2  7459  mpt2exxg  7477  offval22  7487  fnwelem  7526  tposexg  7601  pmex  8097  mapex  8098  pmvalg  8103  elpmg  8108  fvdiagfn  8139  ixpexg  8169  snmapen  8273  xpdom2  8294  xpdom3  8297  omxpen  8301  fodomr  8350  disjenex  8357  domssex2  8359  domssex  8360  mapxpen  8365  xpfi  8470  fczfsuppd  8532  marypha1  8579  brwdom2  8717  wdom2d  8724  xpwdomg  8729  unxpwdom2  8732  ixpiunwdom  8735  djuex  9018  djuexALT  9031  fseqen  9133  cdaval  9277  cdaassen  9289  mapcdaen  9291  cdadom1  9293  cdainf  9299  hsmexlem2  9534  axdc2lem  9555  fnct  9644  iundom2g  9647  fpwwe2lem2  9739  fpwwe2lem5  9741  fpwwe2lem12  9748  fpwwe2lem13  9749  fpwwelem  9752  canthwe  9758  pwxpndom  9773  gchhar  9786  wrdexg  13526  trclexlem  13958  pwsbas  16352  pwsle  16357  pwssca  16361  isacs1i  16522  rescval2  16692  reschom  16694  rescabs  16697  setccofval  16936  isga  17925  sylow2a  18235  lsmhash  18319  efgtf  18336  frgpcpbl  18373  frgp0  18374  frgpeccl  18375  frgpadd  18377  frgpmhm  18379  vrgpf  18382  vrgpinv  18383  frgpupf  18387  frgpup1  18389  frgpup2  18390  frgpup3lem  18391  frgpnabllem1  18477  frgpnabllem2  18478  gsum2d2  18574  gsumcom2  18575  gsumxp  18576  dprd2da  18643  pwssplit3  19268  opsrval  19683  opsrtoslem2  19693  evlslem4  19716  mpt2frlmd  20326  frlmip  20327  matbas2d  20439  mattposvs  20472  mat1dimelbas  20488  mdetrlin  20619  lmfval  21250  txbasex  21583  txopn  21619  txcn  21643  txrest  21648  txindislem  21650  xkoinjcn  21704  tsmsxp  22171  ustssel  22222  ustfilxp  22229  trust  22246  restutop  22254  trcfilu  22311  cfiluweak  22312  imasdsf1olem  22391  blfvalps  22401  metustfbas  22575  restmetu  22588  bcthlem1  23333  bcthlem5  23337  rrxip  23390  perpln1  25819  perpln2  25820  isperp  25821  isleag  25947  isvcOLD  27762  resf1o  29832  locfinref  30233  metidval  30258  esum2dlem  30479  esum2d  30480  esumiun  30481  elsx  30582  madeval  32256  filnetlem3  32696  filnetlem4  32697  bj-xpexg2  33257  isrngod  34008  isgrpda  34065  iscringd  34108  inxpex  34422  xrninxpex  34465  wdom2d2  38103  unxpwdom3  38166  trclubgNEW  38425  relexpxpnnidm  38495  relexpxpmin  38509  enrelmap  38791  rfovd  38795  rfovcnvf1od  38798  fsovrfovd  38803  xpexd  39777  dvsinax  40607  sge0xp  41125  mpt2exxg2  42684