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

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

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 5070 . 2
2 unexg 6514 . . 3
3 pwexg 4593 . . 3
4 pwexg 4593 . . 3
52, 3, 43syl 20 . 2
6 ssexg 4555 . 2
71, 5, 6sylancr 663 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1758   cvv 3081  u.cun 3440  C_wss 3442  ~Pcpw 3976  X.cxp 4955
This theorem is referenced by:  xpex  6641  resiexg  6647  opabex2  6649  cnvexg  6657  coexg  6661  fex2  6665  fabexg  6666  resfunexgALT  6673  cofunexg  6674  fnexALT  6676  opabex3d  6688  opabex3  6689  oprabexd  6697  ofmresex  6707  mpt2exxg  6780  offval22  6785  fnwelem  6821  tposexg  6893  erex  7259  pmex  7353  mapex  7354  pmvalg  7359  elpmg  7362  fvdiagfn  7391  ixpexg  7421  map1  7522  xpdom2  7540  xpdom3  7543  omxpen  7547  fodomr  7596  disjenex  7603  domssex2  7605  domssex  7606  mapxpen  7611  xpfi  7718  fczfsuppd  7773  marypha1  7820  hartogslem2  7894  brwdom2  7925  wdom2d  7932  xpwdomg  7937  unxpwdom2  7940  harwdom  7942  ixpiunwdom  7943  fseqen  8334  dfac8b  8338  ac10ct  8341  cdaval  8476  cdaassen  8488  mapcdaen  8490  cdadom1  8492  cdainf  8498  hsmexlem2  8733  axdc2lem  8754  iundom2g  8841  fpwwe2lem2  8936  fpwwe2lem5  8938  fpwwe2lem12  8945  fpwwe2lem13  8946  fpwwelem  8949  canthwe  8955  pwxpndom  8970  gchhar  8983  wrdexg  12402  pwsbas  14584  pwsle  14589  pwssca  14593  isacs1i  14754  ssclem  14891  rescval2  14900  reschom  14902  rescabs  14905  setccofval  15109  ipolerval  15485  isga  15968  sylow2a  16279  lsmhash  16363  efgtf  16380  frgpcpbl  16417  frgp0  16418  frgpeccl  16419  frgpadd  16421  frgpmhm  16423  vrgpf  16426  vrgpinv  16427  frgpupf  16431  frgpup1  16433  frgpup2  16434  frgpup3lem  16435  frgpnabllem1  16512  frgpnabllem2  16513  gsum2d2  16635  gsumcom2  16636  gsumxp  16637  gsumxpOLD  16639  dprd2da  16716  pwssplit3  17318  opsrval  17733  opsrtoslem2  17743  evlslem4  17768  mpt2frlmd  18395  frlmip  18396  mat0op  18508  matbas2d  18512  matecl  18514  matlmod  18518  mattposvs  18544  mat1dimelbas  18560  mdetrlin  18676  lmfval  19235  txbasex  19538  txopn  19574  txcn  19598  txrest  19603  txindislem  19605  xkoinjcn  19659  tsmsxp  20128  ustval  20176  isust  20177  ustssel  20179  ustfilxp  20186  trust  20203  restutop  20211  restutopopn  20212  ressuss  20237  trcfilu  20268  cfiluweak  20269  ispsmet  20279  ismet  20297  isxmet  20298  imasdsf1olem  20347  blfvalps  20357  metustfbasOLD  20539  metustfbas  20540  restmetu  20561  bcthlem1  21234  bcthlem5  21238  rrxip  21293  perpln1  23531  perpln2  23532  isperp  23533  isgrp2d  24191  isgrpda  24253  isrngod  24335  isvc  24428  fnct  26480  resf1o  26497  metidval  26774  elsx  27065  fin2so  28876  filnetlem3  29061  filnetlem4  29062  iscringd  29259  wdom2d2  29844  unxpwdom3  29908  dvsinax  30470  3xpexg  30997  2wlkonot  31261  2spthonot  31262  2spotmdisj  31538  mpt2exxg2  31602  bj-xpexg2  33297  bj-diagval  33376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2806  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-opab 4468  df-xp 4963
  Copyright terms: Public domain W3C validator