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

Theorem xpexg 4929
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6236. (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 4926 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4650 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4324 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4324 . . 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 4290 . 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 1717   _Vcvv 2899    u. cun 3261    C_ wss 3263   ~Pcpw 3742    X. cxp 4816
This theorem is referenced by:  xpex  4930  resiexg  5128  cnvexg  5345  coexg  5352  fex2  5543  fabexg  5564  resfunexgALT  5897  cofunexg  5898  fnexALT  5901  opabex3d  5928  opabex3  5929  oprabexd  6125  ofmresex  6284  mpt2exxg  6361  fnwelem  6397  tposexg  6429  erex  6865  pmex  6959  mapex  6960  pmvalg  6965  elpmg  6968  fvdiagfn  6994  ixpexg  7022  map1  7121  xpdom2  7139  xpdom3  7142  omxpen  7146  fodomr  7194  disjenex  7201  domssex2  7203  domssex  7204  mapxpen  7209  xpfi  7314  marypha1  7374  hartogslem2  7445  brwdom2  7474  wdom2d  7481  xpwdomg  7486  unxpwdom2  7489  harwdom  7491  ixpiunwdom  7492  fseqen  7841  dfac8b  7845  ac10ct  7848  cdaval  7983  cdaassen  7995  mapcdaen  7997  cdadom1  7999  cdainf  8005  hsmexlem2  8240  axdc2lem  8261  iundom2g  8348  fpwwe2lem2  8440  fpwwe2lem5  8442  fpwwe2lem12  8449  fpwwe2lem13  8450  fpwwelem  8453  canthwe  8459  pwxpndom  8474  gchhar  8479  wrdexg  11666  pwsbas  13636  pwsle  13641  pwssca  13645  isacs1i  13809  ssclem  13946  rescval2  13955  reschom  13957  rescabs  13960  setccofval  14164  ipolerval  14509  isga  14995  sylow2a  15180  lsmhash  15264  efgtf  15281  frgpcpbl  15318  frgp0  15319  frgpeccl  15320  frgpadd  15322  frgpmhm  15324  vrgpf  15327  vrgpinv  15328  frgpupf  15332  frgpup1  15334  frgpup2  15335  frgpup3lem  15336  frgpnabllem1  15411  frgpnabllem2  15412  gsum2d2  15475  gsumcom2  15476  gsumxp  15477  dprd2da  15527  opsrval  16462  opsrtoslem2  16472  lmfval  17218  txbasex  17519  txopn  17555  txcn  17579  txrest  17584  txindislem  17586  xkoinjcn  17640  tsmsxp  18105  ustval  18153  isust  18154  ustssel  18156  ustfilxp  18163  trust  18180  restutop  18188  restutopopn  18189  ressuss  18214  trcfilu  18245  cfiluweak  18246  ismet  18262  isxmet  18263  imasdsf1olem  18311  blfval  18321  metustfbas  18477  restmetu  18489  bcthlem1  19146  bcthlem5  19150  isgrp2d  21671  isgrpda  21733  isrngod  21815  isvc  21908  fnct  23946  elsx  24344  filnetlem3  26100  filnetlem4  26101  iscringd  26300  wdom2d2  26797  pwssplit3  26859  unxpwdom3  26925  matlmod  27148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-rex 2655  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-opab 4208  df-xp 4824
  Copyright terms: Public domain W3C validator