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

Theorem xpexg 4816
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6086. (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 4813 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4537 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4210 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4210 . . 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 4176 . 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 644 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   _Vcvv 2801    u. cun 3163    C_ wss 3165   ~Pcpw 3638    X. cxp 4703
This theorem is referenced by:  xpex  4817  resiexg  5013  cnvexg  5224  coexg  5231  fex2  5417  fabexg  5438  resfunexgALT  5754  cofunexg  5755  fnexALT  5758  opabex3  5785  oprabexd  5976  ofmresex  6134  mpt2exxg  6211  fnwelem  6246  tposexg  6264  erex  6700  pmex  6793  mapex  6794  pmvalg  6799  elpmg  6802  fvdiagfn  6828  ixpexg  6856  map1  6955  xpdom2  6973  xpdom3  6976  omxpen  6980  fodomr  7028  disjenex  7035  domssex2  7037  domssex  7038  mapxpen  7043  xpfi  7144  marypha1  7203  hartogslem2  7274  brwdom2  7303  wdom2d  7310  xpwdomg  7315  unxpwdom2  7318  harwdom  7320  ixpiunwdom  7321  fseqen  7670  dfac8b  7674  ac10ct  7677  cdaval  7812  cdaassen  7824  mapcdaen  7826  cdadom1  7828  cdainf  7834  hsmexlem2  8069  axdc2lem  8090  iundom2g  8178  fpwwe2lem2  8270  fpwwe2lem5  8272  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwelem  8283  canthwe  8289  pwxpndom  8304  gchhar  8309  wrdexg  11441  pwsbas  13402  pwsle  13407  pwssca  13411  isacs1i  13575  ssclem  13712  rescval2  13721  reschom  13723  rescabs  13726  setccofval  13930  ipolerval  14275  isga  14761  sylow2a  14946  lsmhash  15030  efgtf  15047  frgpcpbl  15084  frgp0  15085  frgpeccl  15086  frgpadd  15088  frgpmhm  15090  vrgpf  15093  vrgpinv  15094  frgpupf  15098  frgpup1  15100  frgpup2  15101  frgpup3lem  15102  frgpnabllem1  15177  frgpnabllem2  15178  gsum2d2  15241  gsumcom2  15242  gsumxp  15243  dprd2da  15293  opsrval  16232  opsrtoslem2  16242  lmfval  16978  txbasex  17277  txopn  17313  txcn  17336  txrest  17341  txindislem  17343  xkoinjcn  17397  tsmsxp  17853  ismet  17904  isxmet  17905  imasdsf1olem  17953  blfval  17963  bcthlem1  18762  bcthlem5  18766  isgrp2d  20918  isgrpda  20980  isrngod  21062  isvc  21153  fnct  23356  elsx  23540  cur1vald  25302  domrancur1b  25303  domrancur1clem  25304  domrancur1c  25305  valcurfn1  25307  sqpre  25341  inposet  25381  prismorcsetlem  26015  prismorcset  26017  lemindclsbu  26098  filnetlem3  26432  filnetlem4  26433  iscringd  26727  wdom2d2  27231  pwssplit3  27293  unxpwdom3  27359  matlmod  27582  opabex3d  28190
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rex 2562  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator