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

Theorem xpexg 4707
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 4704 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 4412 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4088 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4088 . . 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 4057 . 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 2727    u. cun 3076    C_ wss 3078   ~Pcpw 3530    X. cxp 4578
This theorem is referenced by:  xpex  4708  resiexg  4904  cnvexg  5114  coexg  5121  fex2  5258  fabexg  5279  resfunexgALT  5590  cofunexg  5591  fnexALT  5594  opabex3  5621  oprabexd  5812  ofmresex  5970  mpt2exxg  6047  fnwelem  6082  tposexg  6100  erex  6570  pmex  6663  mapex  6664  pmvalg  6669  elpmg  6672  fvdiagfn  6698  ixpexg  6726  map1  6824  xpdom2  6842  xpdom3  6845  omxpen  6849  fodomr  6897  disjenex  6904  domssex2  6906  domssex  6907  mapxpen  6912  xpfi  7013  marypha1  7071  hartogslem2  7142  brwdom2  7171  wdom2d  7178  xpwdomg  7183  unxpwdom2  7186  harwdom  7188  ixpiunwdom  7189  fseqen  7538  dfac8b  7542  ac10ct  7545  cdaval  7680  cdaassen  7692  mapcdaen  7694  cdadom1  7696  cdainf  7702  axdc2lem  7958  iundom2g  8046  fpwwe2lem2  8134  fpwwe2lem5  8136  fpwwe2lem12  8143  fpwwe2lem13  8144  fpwwelem  8147  canthwe  8153  pwxpndom  8168  gchhar  8173  wrdexg  11302  pwsbas  13260  pwsle  13265  pwssca  13269  isacs1i  13403  ssclem  13540  rescval2  13549  reschom  13551  rescabs  13554  setccofval  13758  ipolerval  14103  isga  14580  sylow2a  14765  lsmhash  14849  efgtf  14866  frgpcpbl  14903  frgp0  14904  frgpeccl  14905  frgpadd  14907  frgpmhm  14909  vrgpf  14912  vrgpinv  14913  frgpupf  14917  frgpup1  14919  frgpup2  14920  frgpup3lem  14921  frgpnabllem1  14996  frgpnabllem2  14997  gsum2d2  15060  gsumcom2  15061  gsumxp  15062  dprd2da  15112  opsrval  16048  opsrtoslem2  16058  lmfval  16794  txbasex  17093  txopn  17129  txcn  17152  txrest  17157  txindislem  17159  xkoinjcn  17213  tsmsxp  17669  ismet  17720  isxmet  17721  imasdsf1olem  17769  blfval  17779  bcthlem1  18578  bcthlem5  18582  isgrp2d  20732  isgrpda  20794  isrngod  20876  isvc  20967  cur1vald  24365  domrancur1b  24366  domrancur1clem  24367  domrancur1c  24368  valcurfn1  24370  sqpre  24404  inposet  24444  prismorcsetlem  25078  prismorcset  25080  lemindclsbu  25161  filnetlem3  25495  filnetlem4  25496  iscringd  25790  wdom2d2  26294  pwssplit3  26356  unxpwdom3  26422  matlmod  26645
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rex 2514  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-opab 3975  df-xp 4594
  Copyright terms: Public domain W3C validator