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

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

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 5121 . 2
2 unexg 6601 . . 3
3 pwexg 4636 . . 3
4 pwexg 4636 . . 3
52, 3, 43syl 20 . 2
6 ssexg 4598 . 2
71, 5, 6sylancr 663 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   cvv 3109  u.cun 3473  C_wss 3475  ~Pcpw 4012  X.cxp 5002
This theorem is referenced by:  3xpexg  6603  xpex  6604  sqxpexg  6605  opabex2  6738  cnvexg  6746  coexg  6751  fex2  6755  fabexg  6756  resfunexgALT  6763  cofunexg  6764  fnexALT  6766  opabex3d  6778  opabex3  6779  oprabexd  6787  ofmresex  6797  mpt2exxg  6874  offval22  6879  fnwelem  6915  tposexg  6988  pmex  7444  mapex  7445  pmvalg  7450  elpmg  7454  fvdiagfn  7483  ixpexg  7513  map1  7614  xpdom2  7632  xpdom3  7635  omxpen  7639  fodomr  7688  disjenex  7695  domssex2  7697  domssex  7698  mapxpen  7703  xpfi  7811  fczfsuppd  7867  marypha1  7914  brwdom2  8020  wdom2d  8027  xpwdomg  8032  unxpwdom2  8035  ixpiunwdom  8038  fseqen  8429  cdaval  8571  cdaassen  8583  mapcdaen  8585  cdadom1  8587  cdainf  8593  hsmexlem2  8828  axdc2lem  8849  iundom2g  8936  fpwwe2lem2  9031  fpwwe2lem5  9033  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwelem  9044  canthwe  9050  pwxpndom  9065  gchhar  9078  wrdexg  12557  pwsbas  14884  pwsle  14889  pwssca  14893  isacs1i  15054  rescval2  15197  reschom  15199  rescabs  15202  setccofval  15409  isga  16329  sylow2a  16639  lsmhash  16723  efgtf  16740  frgpcpbl  16777  frgp0  16778  frgpeccl  16779  frgpadd  16781  frgpmhm  16783  vrgpf  16786  vrgpinv  16787  frgpupf  16791  frgpup1  16793  frgpup2  16794  frgpup3lem  16795  frgpnabllem1  16877  frgpnabllem2  16878  gsum2d2  17002  gsumcom2  17003  gsumxp  17004  gsumxpOLD  17006  dprd2da  17091  pwssplit3  17707  opsrval  18139  opsrtoslem2  18149  evlslem4  18174  mpt2frlmd  18808  frlmip  18809  matbas2d  18925  mattposvs  18957  mat1dimelbas  18973  mdetrlin  19104  lmfval  19733  txbasex  20067  txopn  20103  txcn  20127  txrest  20132  txindislem  20134  xkoinjcn  20188  tsmsxp  20657  ustssel  20708  ustfilxp  20715  trust  20732  restutop  20740  trcfilu  20797  cfiluweak  20798  imasdsf1olem  20876  blfvalps  20886  metustfbasOLD  21068  metustfbas  21069  restmetu  21090  bcthlem1  21763  bcthlem5  21767  rrxip  21822  perpln1  24087  perpln2  24088  isperp  24089  isgrp2d  25237  isgrpda  25299  isrngod  25381  isvc  25474  fnct  27536  resf1o  27553  locfinref  27844  metidval  27869  elsx  28165  filnetlem3  30198  filnetlem4  30199  iscringd  30396  wdom2d2  30977  unxpwdom3  31041  dvsinax  31708  mpt2exxg2  32927  bj-xpexg2  34517
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator