MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpexg Unicode version

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

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 4924 . 2
2 unexg 6351 . . 3
3 pwexg 4448 . . 3
4 pwexg 4448 . . 3
52, 3, 43syl 19 . 2
6 ssexg 4413 . 2
71, 5, 6sylancr 648 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  e.wcel 1749   cvv 2951  u.cun 3303  C_wss 3305  ~Pcpw 3837  X.cxp 4809
This theorem is referenced by:  xpex  6478  resiexg  6484  opabex2  6486  cnvexg  6494  coexg  6497  fex2  6501  fabexg  6502  resfunexgALT  6509  cofunexg  6510  fnexALT  6512  opabex3d  6524  opabex3  6525  oprabexd  6533  ofmresex  6543  mpt2exxg  6616  offval22  6621  fnwelem  6656  tposexg  6721  erex  7086  pmex  7180  mapex  7181  pmvalg  7186  elpmg  7189  fvdiagfn  7216  ixpexg  7246  map1  7347  xpdom2  7365  xpdom3  7368  omxpen  7372  fodomr  7421  disjenex  7428  domssex2  7430  domssex  7431  mapxpen  7436  xpfi  7542  fczfsuppd  7594  marypha1  7631  hartogslem2  7704  brwdom2  7735  wdom2d  7742  xpwdomg  7747  unxpwdom2  7750  harwdom  7752  ixpiunwdom  7753  fseqen  8144  dfac8b  8148  ac10ct  8151  cdaval  8286  cdaassen  8298  mapcdaen  8300  cdadom1  8302  cdainf  8308  hsmexlem2  8543  axdc2lem  8564  iundom2g  8651  fpwwe2lem2  8745  fpwwe2lem5  8747  fpwwe2lem12  8754  fpwwe2lem13  8755  fpwwelem  8758  canthwe  8764  pwxpndom  8779  gchhar  8792  wrdexg  12185  pwsbas  14365  pwsle  14370  pwssca  14374  isacs1i  14535  ssclem  14672  rescval2  14681  reschom  14683  rescabs  14686  setccofval  14890  ipolerval  15266  isga  15746  sylow2a  16055  lsmhash  16139  efgtf  16156  frgpcpbl  16193  frgp0  16194  frgpeccl  16195  frgpadd  16197  frgpmhm  16199  vrgpf  16202  vrgpinv  16203  frgpupf  16207  frgpup1  16209  frgpup2  16210  frgpup3lem  16211  frgpnabllem1  16287  frgpnabllem2  16288  gsum2d2  16357  gsumcom2  16358  gsumxp  16359  dprd2da  16409  pwssplit3  16951  opsrval  17358  opsrtoslem2  17368  mpt2frlmd  17906  frlmip  17907  mat0op  18018  matbas2d  18022  matecl  18024  matlmod  18027  mattposvs  18037  mdetrlin  18111  lmfval  18540  txbasex  18843  txopn  18879  txcn  18903  txrest  18908  txindislem  18910  xkoinjcn  18964  tsmsxp  19429  ustval  19477  isust  19478  ustssel  19480  ustfilxp  19487  trust  19504  restutop  19512  restutopopn  19513  ressuss  19538  trcfilu  19569  cfiluweak  19570  ispsmet  19580  ismet  19598  isxmet  19599  imasdsf1olem  19648  blfvalps  19658  metustfbasOLD  19840  metustfbas  19841  restmetu  19862  bcthlem1  20535  bcthlem5  20539  rrxip  20594  isgrp2d  23401  isgrpda  23463  isrngod  23545  isvc  23638  fnct  25693  resf1o  25710  metidval  26026  elsx  26317  fin2so  28087  filnetlem3  28272  filnetlem4  28273  iscringd  28470  wdom2d2  29057  unxpwdom3  29121  3xpexg  29794  2wlkonot  30058  2spthonot  30059  2spotmdisj  30335  mpt2exxg2  30400  gsumX2d2  30506  gsumXcom2  30507  gsumXxp  30508  bj-xpexg2  31899  bj-diagval  31969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-rex 2700  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-opab 4326  df-xp 4817
  Copyright terms: Public domain W3C validator