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

Theorem xpexg 4948
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6256. (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 4945 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4669 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4343 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4343 . . 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 4309 . 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 1721   _Vcvv 2916    u. cun 3278    C_ wss 3280   ~Pcpw 3759    X. cxp 4835
This theorem is referenced by:  xpex  4949  resiexg  5147  cnvexg  5364  coexg  5371  fex2  5562  fabexg  5583  resfunexgALT  5917  cofunexg  5918  fnexALT  5921  opabex3d  5948  opabex3  5949  oprabexd  6145  ofmresex  6304  mpt2exxg  6381  fnwelem  6420  tposexg  6452  erex  6888  pmex  6982  mapex  6983  pmvalg  6988  elpmg  6991  fvdiagfn  7017  ixpexg  7045  map1  7144  xpdom2  7162  xpdom3  7165  omxpen  7169  fodomr  7217  disjenex  7224  domssex2  7226  domssex  7227  mapxpen  7232  xpfi  7337  marypha1  7397  hartogslem2  7468  brwdom2  7497  wdom2d  7504  xpwdomg  7509  unxpwdom2  7512  harwdom  7514  ixpiunwdom  7515  fseqen  7864  dfac8b  7868  ac10ct  7871  cdaval  8006  cdaassen  8018  mapcdaen  8020  cdadom1  8022  cdainf  8028  hsmexlem2  8263  axdc2lem  8284  iundom2g  8371  fpwwe2lem2  8463  fpwwe2lem5  8465  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwelem  8476  canthwe  8482  pwxpndom  8497  gchhar  8502  wrdexg  11694  pwsbas  13664  pwsle  13669  pwssca  13673  isacs1i  13837  ssclem  13974  rescval2  13983  reschom  13985  rescabs  13988  setccofval  14192  ipolerval  14537  isga  15023  sylow2a  15208  lsmhash  15292  efgtf  15309  frgpcpbl  15346  frgp0  15347  frgpeccl  15348  frgpadd  15350  frgpmhm  15352  vrgpf  15355  vrgpinv  15356  frgpupf  15360  frgpup1  15362  frgpup2  15363  frgpup3lem  15364  frgpnabllem1  15439  frgpnabllem2  15440  gsum2d2  15503  gsumcom2  15504  gsumxp  15505  dprd2da  15555  opsrval  16490  opsrtoslem2  16500  lmfval  17250  txbasex  17551  txopn  17587  txcn  17611  txrest  17616  txindislem  17618  xkoinjcn  17672  tsmsxp  18137  ustval  18185  isust  18186  ustssel  18188  ustfilxp  18195  trust  18212  restutop  18220  restutopopn  18221  ressuss  18246  trcfilu  18277  cfiluweak  18278  ispsmet  18288  ismet  18306  isxmet  18307  imasdsf1olem  18356  blfvalps  18366  metustfbasOLD  18548  metustfbas  18549  restmetu  18570  bcthlem1  19230  bcthlem5  19234  isgrp2d  21776  isgrpda  21838  isrngod  21920  isvc  22013  fnct  24058  metidval  24238  elsx  24501  filnetlem3  26299  filnetlem4  26300  iscringd  26499  wdom2d2  26996  pwssplit3  27058  unxpwdom3  27124  matlmod  27347  3xpexg  27942  2wlkonot  28062  2spthonot  28063  2spotmdisj  28171
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-opab 4227  df-xp 4843
  Copyright terms: Public domain W3C validator