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

Theorem xpexg 4788
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 4785 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4493 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4166 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4166 . . 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 4134 . 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 647 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 1621   _Vcvv 2763    u. cun 3125    C_ wss 3127   ~Pcpw 3599    X. cxp 4659
This theorem is referenced by:  xpex  4789  resiexg  4985  cnvexg  5195  coexg  5202  fex2  5339  fabexg  5360  resfunexgALT  5672  cofunexg  5673  fnexALT  5676  opabex3  5703  oprabexd  5894  ofmresex  6052  mpt2exxg  6129  fnwelem  6164  tposexg  6182  erex  6652  pmex  6745  mapex  6746  pmvalg  6751  elpmg  6754  fvdiagfn  6780  ixpexg  6808  map1  6907  xpdom2  6925  xpdom3  6928  omxpen  6932  fodomr  6980  disjenex  6987  domssex2  6989  domssex  6990  mapxpen  6995  xpfi  7096  marypha1  7155  hartogslem2  7226  brwdom2  7255  wdom2d  7262  xpwdomg  7267  unxpwdom2  7270  harwdom  7272  ixpiunwdom  7273  fseqen  7622  dfac8b  7626  ac10ct  7629  cdaval  7764  cdaassen  7776  mapcdaen  7778  cdadom1  7780  cdainf  7786  axdc2lem  8042  iundom2g  8130  fpwwe2lem2  8222  fpwwe2lem5  8224  fpwwe2lem12  8231  fpwwe2lem13  8232  fpwwelem  8235  canthwe  8241  pwxpndom  8256  gchhar  8261  wrdexg  11390  pwsbas  13348  pwsle  13353  pwssca  13357  isacs1i  13521  ssclem  13658  rescval2  13667  reschom  13669  rescabs  13672  setccofval  13876  ipolerval  14221  isga  14707  sylow2a  14892  lsmhash  14976  efgtf  14993  frgpcpbl  15030  frgp0  15031  frgpeccl  15032  frgpadd  15034  frgpmhm  15036  vrgpf  15039  vrgpinv  15040  frgpupf  15044  frgpup1  15046  frgpup2  15047  frgpup3lem  15048  frgpnabllem1  15123  frgpnabllem2  15124  gsum2d2  15187  gsumcom2  15188  gsumxp  15189  dprd2da  15239  opsrval  16178  opsrtoslem2  16188  lmfval  16924  txbasex  17223  txopn  17259  txcn  17282  txrest  17287  txindislem  17289  xkoinjcn  17343  tsmsxp  17799  ismet  17850  isxmet  17851  imasdsf1olem  17899  blfval  17909  bcthlem1  18708  bcthlem5  18712  isgrp2d  20862  isgrpda  20924  isrngod  21006  isvc  21097  cur1vald  24566  domrancur1b  24567  domrancur1clem  24568  domrancur1c  24569  valcurfn1  24571  sqpre  24605  inposet  24645  prismorcsetlem  25279  prismorcset  25281  lemindclsbu  25362  filnetlem3  25696  filnetlem4  25697  iscringd  25991  wdom2d2  26495  pwssplit3  26557  unxpwdom3  26623  matlmod  26846
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rex 2524  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-opab 4052  df-xp 4675
  Copyright terms: Public domain W3C validator