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

Theorem xpexg 6599
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6792. (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 4960 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6598 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4601 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4601 . . 3  |-  ( ~P ( A  u.  B
)  e.  _V  ->  ~P ~P ( A  u.  B )  e.  _V )
52, 3, 43syl 18 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ~P ~P ( A  u.  B )  e. 
_V )
6 ssexg 4563 . 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 667 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1867   _Vcvv 3078    u. cun 3431    C_ wss 3433   ~Pcpw 3976    X. cxp 4844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-opab 4477  df-xp 4852  df-rel 4853
This theorem is referenced by:  3xpexg  6600  xpex  6601  sqxpexg  6602  opabex2  6737  cnvexg  6745  coexg  6750  fex2  6754  fabexg  6755  resfunexgALT  6762  cofunexg  6763  fnexALT  6765  opabex3d  6777  opabex3  6778  oprabexd  6786  ofmresex  6796  mpt2exxg  6873  offval22  6878  fnwelem  6914  tposexg  6987  pmex  7477  mapex  7478  pmvalg  7483  elpmg  7487  fvdiagfn  7516  ixpexg  7546  map1  7647  xpdom2  7665  xpdom3  7668  omxpen  7672  fodomr  7721  disjenex  7728  domssex2  7730  domssex  7731  mapxpen  7736  xpfi  7840  fczfsuppd  7899  marypha1  7946  brwdom2  8086  wdom2d  8093  xpwdomg  8098  unxpwdom2  8101  ixpiunwdom  8104  fseqen  8454  cdaval  8596  cdaassen  8608  mapcdaen  8610  cdadom1  8612  cdainf  8618  hsmexlem2  8853  axdc2lem  8874  iundom2g  8961  fpwwe2lem2  9053  fpwwe2lem5  9055  fpwwe2lem12  9062  fpwwe2lem13  9063  fpwwelem  9066  canthwe  9072  pwxpndom  9087  gchhar  9100  wrdexg  12665  trclexlem  13037  pwsbas  15363  pwsle  15368  pwssca  15372  isacs1i  15541  rescval2  15711  reschom  15713  rescabs  15716  setccofval  15955  isga  16923  sylow2a  17249  lsmhash  17333  efgtf  17350  frgpcpbl  17387  frgp0  17388  frgpeccl  17389  frgpadd  17391  frgpmhm  17393  vrgpf  17396  vrgpinv  17397  frgpupf  17401  frgpup1  17403  frgpup2  17404  frgpup3lem  17405  frgpnabllem1  17487  frgpnabllem2  17488  gsum2d2  17584  gsumcom2  17585  gsumxp  17586  dprd2da  17653  pwssplit3  18262  opsrval  18676  opsrtoslem2  18686  evlslem4  18709  mpt2frlmd  19312  frlmip  19313  matbas2d  19425  mattposvs  19457  mat1dimelbas  19473  mdetrlin  19604  lmfval  20225  txbasex  20558  txopn  20594  txcn  20618  txrest  20623  txindislem  20625  xkoinjcn  20679  tsmsxp  21146  ustssel  21197  ustfilxp  21204  trust  21221  restutop  21229  trcfilu  21286  cfiluweak  21287  imasdsf1olem  21365  blfvalps  21375  metustfbas  21549  restmetu  21562  bcthlem1  22269  bcthlem5  22273  rrxip  22326  perpln1  24732  perpln2  24733  isperp  24734  isleag  24860  isgrp2d  25939  isgrpda  26001  isrngod  26083  isvc  26176  fnct  28282  resf1o  28300  locfinref  28657  metidval  28682  esum2dlem  28902  esum2d  28903  esumiun  28904  elsx  29005  filnetlem3  31022  filnetlem4  31023  bj-xpexg2  31503  iscringd  32140  wdom2d2  35804  unxpwdom3  35867  relexpxpnnidm  36149  relexpxpmin  36163  dvsinax  37570  mpt2exxg2  39183
  Copyright terms: Public domain W3C validator