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

Theorem xpexg 4802
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6072. (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 4799 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4523 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4196 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4196 . . 3  |-  ( ~P ( A  u.  B
)  e.  _V  ->  ~P ~P ( A  u.  B )  e.  _V )
52, 3, 43syl 18 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ~P ~P ( A  u.  B )  e. 
_V )
6 ssexg 4162 . 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 644 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1686   _Vcvv 2790    u. cun 3152    C_ wss 3154   ~Pcpw 3627    X. cxp 4689
This theorem is referenced by:  xpex  4803  resiexg  4999  cnvexg  5210  coexg  5217  fex2  5403  fabexg  5424  resfunexgALT  5740  cofunexg  5741  fnexALT  5744  opabex3  5771  oprabexd  5962  ofmresex  6120  mpt2exxg  6197  fnwelem  6232  tposexg  6250  erex  6686  pmex  6779  mapex  6780  pmvalg  6785  elpmg  6788  fvdiagfn  6814  ixpexg  6842  map1  6941  xpdom2  6959  xpdom3  6962  omxpen  6966  fodomr  7014  disjenex  7021  domssex2  7023  domssex  7024  mapxpen  7029  xpfi  7130  marypha1  7189  hartogslem2  7260  brwdom2  7289  wdom2d  7296  xpwdomg  7301  unxpwdom2  7304  harwdom  7306  ixpiunwdom  7307  fseqen  7656  dfac8b  7660  ac10ct  7663  cdaval  7798  cdaassen  7810  mapcdaen  7812  cdadom1  7814  cdainf  7820  hsmexlem2  8055  axdc2lem  8076  iundom2g  8164  fpwwe2lem2  8256  fpwwe2lem5  8258  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwelem  8269  canthwe  8275  pwxpndom  8290  gchhar  8295  wrdexg  11427  pwsbas  13388  pwsle  13393  pwssca  13397  isacs1i  13561  ssclem  13698  rescval2  13707  reschom  13709  rescabs  13712  setccofval  13916  ipolerval  14261  isga  14747  sylow2a  14932  lsmhash  15016  efgtf  15033  frgpcpbl  15070  frgp0  15071  frgpeccl  15072  frgpadd  15074  frgpmhm  15076  vrgpf  15079  vrgpinv  15080  frgpupf  15084  frgpup1  15086  frgpup2  15087  frgpup3lem  15088  frgpnabllem1  15163  frgpnabllem2  15164  gsum2d2  15227  gsumcom2  15228  gsumxp  15229  dprd2da  15279  opsrval  16218  opsrtoslem2  16228  lmfval  16964  txbasex  17263  txopn  17299  txcn  17322  txrest  17327  txindislem  17329  xkoinjcn  17383  tsmsxp  17839  ismet  17890  isxmet  17891  imasdsf1olem  17939  blfval  17949  bcthlem1  18748  bcthlem5  18752  isgrp2d  20904  isgrpda  20966  isrngod  21048  isvc  21139  fnct  23343  elsx  23527  cur1vald  25210  domrancur1b  25211  domrancur1clem  25212  domrancur1c  25213  valcurfn1  25215  sqpre  25249  inposet  25289  prismorcsetlem  25923  prismorcset  25925  lemindclsbu  26006  filnetlem3  26340  filnetlem4  26341  iscringd  26635  wdom2d2  27139  pwssplit3  27201  unxpwdom3  27267  matlmod  27490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rex 2551  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-opab 4080  df-xp 4697
  Copyright terms: Public domain W3C validator