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

Theorem xpexg 6710
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6777. (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 5115 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6584 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4631 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4631 . . 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 4593 . 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 663 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 1767   _Vcvv 3113    u. cun 3474    C_ wss 3476   ~Pcpw 4010    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2820  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-opab 4506  df-xp 5005
This theorem is referenced by:  3xpexg  6711  xpex  6712  sqxpexg  6713  resiexg  6720  opabex2  6722  cnvexg  6730  coexg  6735  fex2  6739  fabexg  6740  resfunexgALT  6747  cofunexg  6748  fnexALT  6750  opabex3d  6762  opabex3  6763  oprabexd  6771  ofmresex  6781  mpt2exxg  6857  offval22  6862  fnwelem  6898  tposexg  6969  erex  7335  pmex  7425  mapex  7426  pmvalg  7431  elpmg  7434  fvdiagfn  7463  ixpexg  7493  map1  7594  xpdom2  7612  xpdom3  7615  omxpen  7619  fodomr  7668  disjenex  7675  domssex2  7677  domssex  7678  mapxpen  7683  xpfi  7790  fczfsuppd  7846  marypha1  7893  hartogslem2  7967  brwdom2  7998  wdom2d  8005  xpwdomg  8010  unxpwdom2  8013  harwdom  8015  ixpiunwdom  8016  fseqen  8407  dfac8b  8411  ac10ct  8414  cdaval  8549  cdaassen  8561  mapcdaen  8563  cdadom1  8565  cdainf  8571  hsmexlem2  8806  axdc2lem  8827  iundom2g  8914  fpwwe2lem2  9009  fpwwe2lem5  9011  fpwwe2lem12  9018  fpwwe2lem13  9019  fpwwelem  9022  canthwe  9028  pwxpndom  9043  gchhar  9056  wrdexg  12522  pwsbas  14741  pwsle  14746  pwssca  14750  isacs1i  14911  ssclem  15048  rescval2  15057  reschom  15059  rescabs  15062  setccofval  15266  ipolerval  15642  isga  16131  sylow2a  16442  lsmhash  16526  efgtf  16543  frgpcpbl  16580  frgp0  16581  frgpeccl  16582  frgpadd  16584  frgpmhm  16586  vrgpf  16589  vrgpinv  16590  frgpupf  16594  frgpup1  16596  frgpup2  16597  frgpup3lem  16598  frgpnabllem1  16677  frgpnabllem2  16678  gsum2d2  16802  gsumcom2  16803  gsumxp  16804  gsumxpOLD  16806  dprd2da  16890  pwssplit3  17502  opsrval  17926  opsrtoslem2  17936  evlslem4  17961  mpt2frlmd  18591  frlmip  18592  mat0op  18704  matbas2d  18708  matecl  18710  matlmod  18714  mattposvs  18740  mat1dimelbas  18756  mdetrlin  18887  lmfval  19515  txbasex  19818  txopn  19854  txcn  19878  txrest  19883  txindislem  19885  xkoinjcn  19939  tsmsxp  20408  ustval  20456  isust  20457  ustssel  20459  ustfilxp  20466  trust  20483  restutop  20491  restutopopn  20492  ressuss  20517  trcfilu  20548  cfiluweak  20549  ispsmet  20559  ismet  20577  isxmet  20578  imasdsf1olem  20627  blfvalps  20637  metustfbasOLD  20819  metustfbas  20820  restmetu  20841  bcthlem1  21514  bcthlem5  21518  rrxip  21573  perpln1  23811  perpln2  23812  isperp  23813  2wlkonot  24557  2spthonot  24558  2spotmdisj  24761  isgrp2d  24929  isgrpda  24991  isrngod  25073  isvc  25166  fnct  27224  resf1o  27241  metidval  27521  elsx  27821  fin2so  29633  filnetlem3  29817  filnetlem4  29818  iscringd  30015  wdom2d2  30597  unxpwdom3  30661  dvsinax  31257  mpt2exxg2  32011  bj-xpexg2  33607  bj-diagval  33686
  Copyright terms: Public domain W3C validator