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

Theorem xpexg 6620
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6683. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
xpexg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 5064 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6494 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4587 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4587 . . 3  |-  ( ~P ( A  u.  B
)  e.  _V  ->  ~P ~P ( A  u.  B )  e.  _V )
52, 3, 43syl 20 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ~P ~P ( A  u.  B )  e. 
_V )
6 ssexg 4549 . 2  |-  ( ( ( A  X.  B
)  C_  ~P ~P ( A  u.  B
)  /\  ~P ~P ( A  u.  B
)  e.  _V )  ->  ( A  X.  B
)  e.  _V )
71, 5, 6sylancr 663 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1758   _Vcvv 3078    u. cun 3437    C_ wss 3439   ~Pcpw 3971    X. cxp 4949
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 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485
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 2805  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-opab 4462  df-xp 4957
This theorem is referenced by:  xpex  6621  resiexg  6627  opabex2  6629  cnvexg  6637  coexg  6641  fex2  6645  fabexg  6646  resfunexgALT  6653  cofunexg  6654  fnexALT  6656  opabex3d  6668  opabex3  6669  oprabexd  6677  ofmresex  6687  mpt2exxg  6760  offval22  6765  fnwelem  6800  tposexg  6872  erex  7238  pmex  7332  mapex  7333  pmvalg  7338  elpmg  7341  fvdiagfn  7370  ixpexg  7400  map1  7501  xpdom2  7519  xpdom3  7522  omxpen  7526  fodomr  7575  disjenex  7582  domssex2  7584  domssex  7585  mapxpen  7590  xpfi  7697  fczfsuppd  7752  marypha1  7798  hartogslem2  7871  brwdom2  7902  wdom2d  7909  xpwdomg  7914  unxpwdom2  7917  harwdom  7919  ixpiunwdom  7920  fseqen  8311  dfac8b  8315  ac10ct  8318  cdaval  8453  cdaassen  8465  mapcdaen  8467  cdadom1  8469  cdainf  8475  hsmexlem2  8710  axdc2lem  8731  iundom2g  8818  fpwwe2lem2  8913  fpwwe2lem5  8915  fpwwe2lem12  8922  fpwwe2lem13  8923  fpwwelem  8926  canthwe  8932  pwxpndom  8947  gchhar  8960  wrdexg  12365  pwsbas  14547  pwsle  14552  pwssca  14556  isacs1i  14717  ssclem  14854  rescval2  14863  reschom  14865  rescabs  14868  setccofval  15072  ipolerval  15448  isga  15931  sylow2a  16242  lsmhash  16326  efgtf  16343  frgpcpbl  16380  frgp0  16381  frgpeccl  16382  frgpadd  16384  frgpmhm  16386  vrgpf  16389  vrgpinv  16390  frgpupf  16394  frgpup1  16396  frgpup2  16397  frgpup3lem  16398  frgpnabllem1  16475  frgpnabllem2  16476  gsum2d2  16591  gsumcom2  16592  gsumxp  16593  gsumxpOLD  16595  dprd2da  16666  pwssplit3  17268  opsrval  17683  opsrtoslem2  17693  evlslem4  17718  mpt2frlmd  18330  frlmip  18331  mat0op  18448  matbas2d  18452  matecl  18454  matlmod  18458  mattposvs  18469  mdetrlin  18543  lmfval  18971  txbasex  19274  txopn  19310  txcn  19334  txrest  19339  txindislem  19341  xkoinjcn  19395  tsmsxp  19864  ustval  19912  isust  19913  ustssel  19915  ustfilxp  19922  trust  19939  restutop  19947  restutopopn  19948  ressuss  19973  trcfilu  20004  cfiluweak  20005  ispsmet  20015  ismet  20033  isxmet  20034  imasdsf1olem  20083  blfvalps  20093  metustfbasOLD  20275  metustfbas  20276  restmetu  20297  bcthlem1  20970  bcthlem5  20974  rrxip  21029  perpln1  23247  perpln2  23248  isperp  23249  isgrp2d  23894  isgrpda  23956  isrngod  24038  isvc  24131  fnct  26184  resf1o  26201  metidval  26482  elsx  26773  fin2so  28584  filnetlem3  28769  filnetlem4  28770  iscringd  28967  wdom2d2  29552  unxpwdom3  29616  3xpexg  30288  2wlkonot  30552  2spthonot  30553  2spotmdisj  30829  mpt2exxg2  30896  mat1dimelbas  31053  bj-xpexg2  32804  bj-diagval  32883
  Copyright terms: Public domain W3C validator