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

Theorem xpexg 4799
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (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 4796 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4520 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4193 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4193 . . 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 4161 . 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 646 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   _Vcvv 2789    u. cun 3151    C_ wss 3153   ~Pcpw 3626    X. cxp 4686
This theorem is referenced by:  xpex  4800  resiexg  4996  cnvexg  5206  coexg  5213  fex2  5366  fabexg  5387  resfunexgALT  5699  cofunexg  5700  fnexALT  5703  opabex3  5730  oprabexd  5921  ofmresex  6079  mpt2exxg  6156  fnwelem  6191  tposexg  6209  erex  6679  pmex  6772  mapex  6773  pmvalg  6778  elpmg  6781  fvdiagfn  6807  ixpexg  6835  map1  6934  xpdom2  6952  xpdom3  6955  omxpen  6959  fodomr  7007  disjenex  7014  domssex2  7016  domssex  7017  mapxpen  7022  xpfi  7123  marypha1  7182  hartogslem2  7253  brwdom2  7282  wdom2d  7289  xpwdomg  7294  unxpwdom2  7297  harwdom  7299  ixpiunwdom  7300  fseqen  7649  dfac8b  7653  ac10ct  7656  cdaval  7791  cdaassen  7803  mapcdaen  7805  cdadom1  7807  cdainf  7813  axdc2lem  8069  iundom2g  8157  fpwwe2lem2  8249  fpwwe2lem5  8251  fpwwe2lem12  8258  fpwwe2lem13  8259  fpwwelem  8262  canthwe  8268  pwxpndom  8283  gchhar  8288  wrdexg  11419  pwsbas  13380  pwsle  13385  pwssca  13389  isacs1i  13553  ssclem  13690  rescval2  13699  reschom  13701  rescabs  13704  setccofval  13908  ipolerval  14253  isga  14739  sylow2a  14924  lsmhash  15008  efgtf  15025  frgpcpbl  15062  frgp0  15063  frgpeccl  15064  frgpadd  15066  frgpmhm  15068  vrgpf  15071  vrgpinv  15072  frgpupf  15076  frgpup1  15078  frgpup2  15079  frgpup3lem  15080  frgpnabllem1  15155  frgpnabllem2  15156  gsum2d2  15219  gsumcom2  15220  gsumxp  15221  dprd2da  15271  opsrval  16210  opsrtoslem2  16220  lmfval  16956  txbasex  17255  txopn  17291  txcn  17314  txrest  17319  txindislem  17321  xkoinjcn  17375  tsmsxp  17831  ismet  17882  isxmet  17883  imasdsf1olem  17931  blfval  17941  bcthlem1  18740  bcthlem5  18744  isgrp2d  20894  isgrpda  20956  isrngod  21038  isvc  21129  cur1vald  24598  domrancur1b  24599  domrancur1clem  24600  domrancur1c  24601  valcurfn1  24603  sqpre  24637  inposet  24677  prismorcsetlem  25311  prismorcset  25313  lemindclsbu  25394  filnetlem3  25728  filnetlem4  25729  iscringd  26023  wdom2d2  26527  pwssplit3  26589  unxpwdom3  26655  matlmod  26878
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rex 2550  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-opab 4079  df-xp 4694
  Copyright terms: Public domain W3C validator