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

Theorem xpexg 4975
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6283. (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 4972 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4696 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4370 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4370 . . 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 4336 . 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 2943    u. cun 3305    C_ wss 3307   ~Pcpw 3786    X. cxp 4862
This theorem is referenced by:  xpex  4976  resiexg  5174  cnvexg  5391  coexg  5398  fex2  5589  fabexg  5610  resfunexgALT  5944  cofunexg  5945  fnexALT  5948  opabex3d  5975  opabex3  5976  oprabexd  6172  ofmresex  6331  mpt2exxg  6408  fnwelem  6447  tposexg  6479  erex  6915  pmex  7009  mapex  7010  pmvalg  7015  elpmg  7018  fvdiagfn  7044  ixpexg  7072  map1  7171  xpdom2  7189  xpdom3  7192  omxpen  7196  fodomr  7244  disjenex  7251  domssex2  7253  domssex  7254  mapxpen  7259  xpfi  7364  marypha1  7425  hartogslem2  7496  brwdom2  7525  wdom2d  7532  xpwdomg  7537  unxpwdom2  7540  harwdom  7542  ixpiunwdom  7543  fseqen  7892  dfac8b  7896  ac10ct  7899  cdaval  8034  cdaassen  8046  mapcdaen  8048  cdadom1  8050  cdainf  8056  hsmexlem2  8291  axdc2lem  8312  iundom2g  8399  fpwwe2lem2  8491  fpwwe2lem5  8493  fpwwe2lem12  8500  fpwwe2lem13  8501  fpwwelem  8504  canthwe  8510  pwxpndom  8525  gchhar  8530  wrdexg  11722  pwsbas  13692  pwsle  13697  pwssca  13701  isacs1i  13865  ssclem  14002  rescval2  14011  reschom  14013  rescabs  14016  setccofval  14220  ipolerval  14565  isga  15051  sylow2a  15236  lsmhash  15320  efgtf  15337  frgpcpbl  15374  frgp0  15375  frgpeccl  15376  frgpadd  15378  frgpmhm  15380  vrgpf  15383  vrgpinv  15384  frgpupf  15388  frgpup1  15390  frgpup2  15391  frgpup3lem  15392  frgpnabllem1  15467  frgpnabllem2  15468  gsum2d2  15531  gsumcom2  15532  gsumxp  15533  dprd2da  15583  opsrval  16518  opsrtoslem2  16528  lmfval  17279  txbasex  17581  txopn  17617  txcn  17641  txrest  17646  txindislem  17648  xkoinjcn  17702  tsmsxp  18167  ustval  18215  isust  18216  ustssel  18218  ustfilxp  18225  trust  18242  restutop  18250  restutopopn  18251  ressuss  18276  trcfilu  18307  cfiluweak  18308  ispsmet  18318  ismet  18336  isxmet  18337  imasdsf1olem  18386  blfvalps  18396  metustfbasOLD  18578  metustfbas  18579  restmetu  18600  bcthlem1  19260  bcthlem5  19264  isgrp2d  21806  isgrpda  21868  isrngod  21950  isvc  22043  fnct  24088  metidval  24268  elsx  24531  filnetlem3  26341  filnetlem4  26342  iscringd  26541  wdom2d2  27038  pwssplit3  27100  unxpwdom3  27166  matlmod  27389  3xpexg  27984  2wlkonot  28104  2spthonot  28105  2spotmdisj  28213
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 2411  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687
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 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-rex 2698  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-opab 4254  df-xp 4870
  Copyright terms: Public domain W3C validator