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

Theorem xpexg 4981
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6289. (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 4978 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4702 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4375 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4375 . . 3  |-  ( ~P ( A  u.  B
)  e.  _V  ->  ~P ~P ( A  u.  B )  e.  _V )
52, 3, 43syl 19 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ~P ~P ( A  u.  B )  e. 
_V )
6 ssexg 4341 . 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 645 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   _Vcvv 2948    u. cun 3310    C_ wss 3312   ~Pcpw 3791    X. cxp 4868
This theorem is referenced by:  xpex  4982  resiexg  5180  cnvexg  5397  coexg  5404  fex2  5595  fabexg  5616  resfunexgALT  5950  cofunexg  5951  fnexALT  5954  opabex3d  5981  opabex3  5982  oprabexd  6178  ofmresex  6337  mpt2exxg  6414  fnwelem  6453  tposexg  6485  erex  6921  pmex  7015  mapex  7016  pmvalg  7021  elpmg  7024  fvdiagfn  7050  ixpexg  7078  map1  7177  xpdom2  7195  xpdom3  7198  omxpen  7202  fodomr  7250  disjenex  7257  domssex2  7259  domssex  7260  mapxpen  7265  xpfi  7370  marypha1  7431  hartogslem2  7504  brwdom2  7533  wdom2d  7540  xpwdomg  7545  unxpwdom2  7548  harwdom  7550  ixpiunwdom  7551  fseqen  7900  dfac8b  7904  ac10ct  7907  cdaval  8042  cdaassen  8054  mapcdaen  8056  cdadom1  8058  cdainf  8064  hsmexlem2  8299  axdc2lem  8320  iundom2g  8407  fpwwe2lem2  8499  fpwwe2lem5  8501  fpwwe2lem12  8508  fpwwe2lem13  8509  fpwwelem  8512  canthwe  8518  pwxpndom  8533  gchhar  8538  wrdexg  11731  pwsbas  13701  pwsle  13706  pwssca  13710  isacs1i  13874  ssclem  14011  rescval2  14020  reschom  14022  rescabs  14025  setccofval  14229  ipolerval  14574  isga  15060  sylow2a  15245  lsmhash  15329  efgtf  15346  frgpcpbl  15383  frgp0  15384  frgpeccl  15385  frgpadd  15387  frgpmhm  15389  vrgpf  15392  vrgpinv  15393  frgpupf  15397  frgpup1  15399  frgpup2  15400  frgpup3lem  15401  frgpnabllem1  15476  frgpnabllem2  15477  gsum2d2  15540  gsumcom2  15541  gsumxp  15542  dprd2da  15592  opsrval  16527  opsrtoslem2  16537  lmfval  17288  txbasex  17590  txopn  17626  txcn  17650  txrest  17655  txindislem  17657  xkoinjcn  17711  tsmsxp  18176  ustval  18224  isust  18225  ustssel  18227  ustfilxp  18234  trust  18251  restutop  18259  restutopopn  18260  ressuss  18285  trcfilu  18316  cfiluweak  18317  ispsmet  18327  ismet  18345  isxmet  18346  imasdsf1olem  18395  blfvalps  18405  metustfbasOLD  18587  metustfbas  18588  restmetu  18609  bcthlem1  19269  bcthlem5  19273  isgrp2d  21815  isgrpda  21877  isrngod  21959  isvc  22052  fnct  24097  metidval  24277  elsx  24540  filnetlem3  26400  filnetlem4  26401  iscringd  26600  wdom2d2  27097  pwssplit3  27158  unxpwdom3  27224  matlmod  27447  3xpexg  28044  2wlkonot  28285  2spthonot  28286  2spotmdisj  28394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-opab 4259  df-xp 4876
  Copyright terms: Public domain W3C validator