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

Theorem xpexg 6583
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 6776. (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 4936 . 2  |-  ( A  X.  B )  C_  ~P ~P ( A  u.  B )
2 unexg 6582 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
3 pwexg 4577 . . 3  |-  ( ( A  u.  B )  e.  _V  ->  ~P ( A  u.  B
)  e.  _V )
4 pwexg 4577 . . 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 4539 . 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 661 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842   _Vcvv 3058    u. cun 3411    C_ wss 3413   ~Pcpw 3954    X. cxp 4820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-opab 4453  df-xp 4828  df-rel 4829
This theorem is referenced by:  3xpexg  6584  xpex  6585  sqxpexg  6586  opabex2  6721  cnvexg  6729  coexg  6734  fex2  6738  fabexg  6739  resfunexgALT  6746  cofunexg  6747  fnexALT  6749  opabex3d  6761  opabex3  6762  oprabexd  6770  ofmresex  6780  mpt2exxg  6857  offval22  6862  fnwelem  6898  tposexg  6971  pmex  7461  mapex  7462  pmvalg  7467  elpmg  7471  fvdiagfn  7500  ixpexg  7530  map1  7631  xpdom2  7649  xpdom3  7652  omxpen  7656  fodomr  7705  disjenex  7712  domssex2  7714  domssex  7715  mapxpen  7720  xpfi  7824  fczfsuppd  7880  marypha1  7927  brwdom2  8032  wdom2d  8039  xpwdomg  8044  unxpwdom2  8047  ixpiunwdom  8050  fseqen  8439  cdaval  8581  cdaassen  8593  mapcdaen  8595  cdadom1  8597  cdainf  8603  hsmexlem2  8838  axdc2lem  8859  iundom2g  8946  fpwwe2lem2  9039  fpwwe2lem5  9041  fpwwe2lem12  9048  fpwwe2lem13  9049  fpwwelem  9052  canthwe  9058  pwxpndom  9073  gchhar  9086  wrdexg  12607  trclexlem  12975  pwsbas  15099  pwsle  15104  pwssca  15108  isacs1i  15269  rescval2  15439  reschom  15441  rescabs  15444  setccofval  15683  isga  16651  sylow2a  16961  lsmhash  17045  efgtf  17062  frgpcpbl  17099  frgp0  17100  frgpeccl  17101  frgpadd  17103  frgpmhm  17105  vrgpf  17108  vrgpinv  17109  frgpupf  17113  frgpup1  17115  frgpup2  17116  frgpup3lem  17117  frgpnabllem1  17199  frgpnabllem2  17200  gsum2d2  17321  gsumcom2  17322  gsumxp  17323  dprd2da  17409  pwssplit3  18025  opsrval  18457  opsrtoslem2  18467  evlslem4  18492  mpt2frlmd  19102  frlmip  19103  matbas2d  19215  mattposvs  19247  mat1dimelbas  19263  mdetrlin  19394  lmfval  20024  txbasex  20357  txopn  20393  txcn  20417  txrest  20422  txindislem  20424  xkoinjcn  20478  tsmsxp  20947  ustssel  20998  ustfilxp  21005  trust  21022  restutop  21030  trcfilu  21087  cfiluweak  21088  imasdsf1olem  21166  blfvalps  21176  metustfbasOLD  21358  metustfbas  21359  restmetu  21380  bcthlem1  22053  bcthlem5  22057  rrxip  22112  perpln1  24470  perpln2  24471  isperp  24472  isgrp2d  25637  isgrpda  25699  isrngod  25781  isvc  25874  fnct  27968  resf1o  27986  locfinref  28283  metidval  28308  esum2dlem  28525  esum2d  28526  esumiun  28527  elsx  28628  filnetlem3  30595  filnetlem4  30596  bj-xpexg2  31069  iscringd  31658  wdom2d2  35319  unxpwdom3  35383  relexpxpnnidm  35662  relexpxpmin  35676  dvsinax  37057  mpt2exxg2  38419
  Copyright terms: Public domain W3C validator