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

Theorem xpexg 6587
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6778. (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 5106 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6586 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4621 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4621 . . 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 4583 . 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 1804   _Vcvv 3095    u. cun 3459    C_ wss 3461   ~Pcpw 3997    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rex 2799  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-opab 4496  df-xp 4995
This theorem is referenced by:  3xpexg  6588  xpex  6589  sqxpexg  6590  opabex2  6723  cnvexg  6731  coexg  6736  fex2  6740  fabexg  6741  resfunexgALT  6748  cofunexg  6749  fnexALT  6751  opabex3d  6763  opabex3  6764  oprabexd  6772  ofmresex  6782  mpt2exxg  6859  offval22  6864  fnwelem  6900  tposexg  6971  pmex  7427  mapex  7428  pmvalg  7433  elpmg  7436  fvdiagfn  7465  ixpexg  7495  map1  7596  xpdom2  7614  xpdom3  7617  omxpen  7621  fodomr  7670  disjenex  7677  domssex2  7679  domssex  7680  mapxpen  7685  xpfi  7793  fczfsuppd  7849  marypha1  7896  brwdom2  8002  wdom2d  8009  xpwdomg  8014  unxpwdom2  8017  ixpiunwdom  8020  fseqen  8411  cdaval  8553  cdaassen  8565  mapcdaen  8567  cdadom1  8569  cdainf  8575  hsmexlem2  8810  axdc2lem  8831  iundom2g  8918  fpwwe2lem2  9013  fpwwe2lem5  9015  fpwwe2lem12  9022  fpwwe2lem13  9023  fpwwelem  9026  canthwe  9032  pwxpndom  9047  gchhar  9060  wrdexg  12539  pwsbas  14866  pwsle  14871  pwssca  14875  isacs1i  15036  rescval2  15179  reschom  15181  rescabs  15184  setccofval  15388  isga  16308  sylow2a  16618  lsmhash  16702  efgtf  16719  frgpcpbl  16756  frgp0  16757  frgpeccl  16758  frgpadd  16760  frgpmhm  16762  vrgpf  16765  vrgpinv  16766  frgpupf  16770  frgpup1  16772  frgpup2  16773  frgpup3lem  16774  frgpnabllem1  16856  frgpnabllem2  16857  gsum2d2  16981  gsumcom2  16982  gsumxp  16983  gsumxpOLD  16985  dprd2da  17070  pwssplit3  17686  opsrval  18118  opsrtoslem2  18128  evlslem4  18153  mpt2frlmd  18786  frlmip  18787  matbas2d  18903  mattposvs  18935  mat1dimelbas  18951  mdetrlin  19082  lmfval  19711  txbasex  20045  txopn  20081  txcn  20105  txrest  20110  txindislem  20112  xkoinjcn  20166  tsmsxp  20635  ustssel  20686  ustfilxp  20693  trust  20710  restutop  20718  trcfilu  20775  cfiluweak  20776  imasdsf1olem  20854  blfvalps  20864  metustfbasOLD  21046  metustfbas  21047  restmetu  21068  bcthlem1  21741  bcthlem5  21745  rrxip  21800  perpln1  24065  perpln2  24066  isperp  24067  isgrp2d  25215  isgrpda  25277  isrngod  25359  isvc  25452  fnct  27514  resf1o  27531  locfinref  27822  metidval  27847  elsx  28143  filnetlem3  30174  filnetlem4  30175  iscringd  30372  wdom2d2  30953  unxpwdom3  31017  dvsinax  31662  mpt2exxg2  32795  bj-xpexg2  34400
  Copyright terms: Public domain W3C validator