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

Theorem xpexg 6496
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6559. (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 4940 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6370 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4464 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4464 . . 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 4426 . 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 656 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   _Vcvv 2962    u. cun 3314    C_ wss 3316   ~Pcpw 3848    X. cxp 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-rex 2711  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-opab 4339  df-xp 4833
This theorem is referenced by:  xpex  6497  resiexg  6503  opabex2  6505  cnvexg  6513  coexg  6517  fex2  6521  fabexg  6522  resfunexgALT  6529  cofunexg  6530  fnexALT  6532  opabex3d  6544  opabex3  6545  oprabexd  6553  ofmresex  6563  mpt2exxg  6636  offval22  6641  fnwelem  6676  tposexg  6748  erex  7113  pmex  7207  mapex  7208  pmvalg  7213  elpmg  7216  fvdiagfn  7245  ixpexg  7275  map1  7376  xpdom2  7394  xpdom3  7397  omxpen  7401  fodomr  7450  disjenex  7457  domssex2  7459  domssex  7460  mapxpen  7465  xpfi  7571  fczfsuppd  7626  marypha1  7672  hartogslem2  7745  brwdom2  7776  wdom2d  7783  xpwdomg  7788  unxpwdom2  7791  harwdom  7793  ixpiunwdom  7794  fseqen  8185  dfac8b  8189  ac10ct  8192  cdaval  8327  cdaassen  8339  mapcdaen  8341  cdadom1  8343  cdainf  8349  hsmexlem2  8584  axdc2lem  8605  iundom2g  8692  fpwwe2lem2  8787  fpwwe2lem5  8789  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwelem  8800  canthwe  8806  pwxpndom  8821  gchhar  8834  wrdexg  12228  pwsbas  14408  pwsle  14413  pwssca  14417  isacs1i  14578  ssclem  14715  rescval2  14724  reschom  14726  rescabs  14729  setccofval  14933  ipolerval  15309  isga  15789  sylow2a  16098  lsmhash  16182  efgtf  16199  frgpcpbl  16236  frgp0  16237  frgpeccl  16238  frgpadd  16240  frgpmhm  16242  vrgpf  16245  vrgpinv  16246  frgpupf  16250  frgpup1  16252  frgpup2  16253  frgpup3lem  16254  frgpnabllem1  16331  frgpnabllem2  16332  gsum2d2  16440  gsumcom2  16441  gsumxp  16442  gsumxpOLD  16444  dprd2da  16515  pwssplit3  17064  opsrval  17488  opsrtoslem2  17498  evlslem4  17519  mpt2frlmd  18044  frlmip  18045  mat0op  18162  matbas2d  18166  matecl  18168  matlmod  18171  mattposvs  18181  mdetrlin  18251  lmfval  18678  txbasex  18981  txopn  19017  txcn  19041  txrest  19046  txindislem  19048  xkoinjcn  19102  tsmsxp  19571  ustval  19619  isust  19620  ustssel  19622  ustfilxp  19629  trust  19646  restutop  19654  restutopopn  19655  ressuss  19680  trcfilu  19711  cfiluweak  19712  ispsmet  19722  ismet  19740  isxmet  19741  imasdsf1olem  19790  blfvalps  19800  metustfbasOLD  19982  metustfbas  19983  restmetu  20004  bcthlem1  20677  bcthlem5  20681  rrxip  20736  isgrp2d  23545  isgrpda  23607  isrngod  23689  isvc  23782  fnct  25837  resf1o  25855  metidval  26171  elsx  26462  fin2so  28260  filnetlem3  28445  filnetlem4  28446  iscringd  28643  wdom2d2  29229  unxpwdom3  29293  3xpexg  29966  2wlkonot  30230  2spthonot  30231  2spotmdisj  30507  mpt2exxg2  30572  bj-xpexg2  32035  bj-diagval  32105
  Copyright terms: Public domain W3C validator