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

Theorem xpexg 6502
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6565. (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 4948 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6376 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4471 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4471 . . 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 4433 . 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 1756   _Vcvv 2967    u. cun 3321    C_ wss 3323   ~Pcpw 3855    X. cxp 4833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rex 2716  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-opab 4346  df-xp 4841
This theorem is referenced by:  xpex  6503  resiexg  6509  opabex2  6511  cnvexg  6519  coexg  6523  fex2  6527  fabexg  6528  resfunexgALT  6535  cofunexg  6536  fnexALT  6538  opabex3d  6550  opabex3  6551  oprabexd  6559  ofmresex  6569  mpt2exxg  6642  offval22  6647  fnwelem  6682  tposexg  6754  erex  7117  pmex  7211  mapex  7212  pmvalg  7217  elpmg  7220  fvdiagfn  7249  ixpexg  7279  map1  7380  xpdom2  7398  xpdom3  7401  omxpen  7405  fodomr  7454  disjenex  7461  domssex2  7463  domssex  7464  mapxpen  7469  xpfi  7575  fczfsuppd  7630  marypha1  7676  hartogslem2  7749  brwdom2  7780  wdom2d  7787  xpwdomg  7792  unxpwdom2  7795  harwdom  7797  ixpiunwdom  7798  fseqen  8189  dfac8b  8193  ac10ct  8196  cdaval  8331  cdaassen  8343  mapcdaen  8345  cdadom1  8347  cdainf  8353  hsmexlem2  8588  axdc2lem  8609  iundom2g  8696  fpwwe2lem2  8791  fpwwe2lem5  8793  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwelem  8804  canthwe  8810  pwxpndom  8825  gchhar  8838  wrdexg  12236  pwsbas  14417  pwsle  14422  pwssca  14426  isacs1i  14587  ssclem  14724  rescval2  14733  reschom  14735  rescabs  14738  setccofval  14942  ipolerval  15318  isga  15800  sylow2a  16109  lsmhash  16193  efgtf  16210  frgpcpbl  16247  frgp0  16248  frgpeccl  16249  frgpadd  16251  frgpmhm  16253  vrgpf  16256  vrgpinv  16257  frgpupf  16261  frgpup1  16263  frgpup2  16264  frgpup3lem  16265  frgpnabllem1  16342  frgpnabllem2  16343  gsum2d2  16454  gsumcom2  16455  gsumxp  16456  gsumxpOLD  16458  dprd2da  16529  pwssplit3  17119  opsrval  17531  opsrtoslem2  17541  evlslem4  17566  mpt2frlmd  18177  frlmip  18178  mat0op  18295  matbas2d  18299  matecl  18301  matlmod  18304  mattposvs  18314  mdetrlin  18384  lmfval  18811  txbasex  19114  txopn  19150  txcn  19174  txrest  19179  txindislem  19181  xkoinjcn  19235  tsmsxp  19704  ustval  19752  isust  19753  ustssel  19755  ustfilxp  19762  trust  19779  restutop  19787  restutopopn  19788  ressuss  19813  trcfilu  19844  cfiluweak  19845  ispsmet  19855  ismet  19873  isxmet  19874  imasdsf1olem  19923  blfvalps  19933  metustfbasOLD  20115  metustfbas  20116  restmetu  20137  bcthlem1  20810  bcthlem5  20814  rrxip  20869  isgrp2d  23673  isgrpda  23735  isrngod  23817  isvc  23910  fnct  25964  resf1o  25981  metidval  26269  elsx  26560  fin2so  28369  filnetlem3  28554  filnetlem4  28555  iscringd  28752  wdom2d2  29337  unxpwdom3  29401  3xpexg  30073  2wlkonot  30337  2spthonot  30338  2spotmdisj  30614  mpt2exxg2  30680  mat1dimelbas  30790  bj-xpexg2  32299  bj-diagval  32372
  Copyright terms: Public domain W3C validator