Theorem xpexg 6960

Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7161. (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

Step	Hyp	Ref	Expression
1		xpsspw 5233	. 2 |- ( A X. B ) C_ ~P ~P ( A u. B )
2		unexg 6959	. . 3 |- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
3		pwexg 4850	. . 3 |- ( ( A u. B ) e. _V -> ~P ( A u. B ) e. _V )
4		pwexg 4850	. . 3 |- ( ~P ( A u. B ) e. _V -> ~P ~P ( A u. B ) e. _V )
5	2, 3, 4	3syl 18	. 2 |- ( ( A e. V /\ B e. W ) -> ~P ~P ( A u. B ) e. _V )
6		ssexg 4804	. 2 |- ( ( ( A X. B ) C_ ~P ~P ( A u. B ) /\ ~P ~P ( A u. B ) e. _V ) -> ( A X. B ) e. _V )
7	1, 5, 6	sylancr 695	1 |- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   _Vcvv 3200   u. cun 3572   C_ wss 3574   ~Pcpw 4158   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  3xpexg  6961  xpex  6962  sqxpexg  6963  cnvexg  7112  coexg  7117  fex2  7121  fabexg  7122  resfunexgALT  7129  cofunexg  7130  fnexALT  7132  opabex3d  7145  opabex3  7146  oprabexd  7155  ofmresex  7165  opabex2  7227  mpt2exxg  7244  offval22  7253  fnwelem  7292  tposexg  7366  pmex  7862  mapex  7863  pmvalg  7868  elpmg  7873  fvdiagfn  7902  ixpexg  7932  map1  8036  xpdom2  8055  xpdom3  8058  omxpen  8062  fodomr  8111  disjenex  8118  domssex2  8120  domssex  8121  mapxpen  8126  xpfi  8231  fczfsuppd  8293  marypha1  8340  brwdom2  8478  wdom2d  8485  xpwdomg  8490  unxpwdom2  8493  ixpiunwdom  8496  fseqen  8850  cdaval  8992  cdaassen  9004  mapcdaen  9006  cdadom1  9008  cdainf  9014  hsmexlem2  9249  axdc2lem  9270  fnct  9359  iundom2g  9362  fpwwe2lem2  9454  fpwwe2lem5  9456  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwelem  9467  canthwe  9473  pwxpndom  9488  gchhar  9501  wrdexg  13315  trclexlem  13733  pwsbas  16147  pwsle  16152  pwssca  16156  isacs1i  16318  rescval2  16488  reschom  16490  rescabs  16493  setccofval  16732  isga  17724  sylow2a  18034  lsmhash  18118  efgtf  18135  frgpcpbl  18172  frgp0  18173  frgpeccl  18174  frgpadd  18176  frgpmhm  18178  vrgpf  18181  vrgpinv  18182  frgpupf  18186  frgpup1  18188  frgpup2  18189  frgpup3lem  18190  frgpnabllem1  18276  frgpnabllem2  18277  gsum2d2  18373  gsumcom2  18374  gsumxp  18375  dprd2da  18441  pwssplit3  19061  opsrval  19474  opsrtoslem2  19485  evlslem4  19508  mpt2frlmd  20116  frlmip  20117  matbas2d  20229  mattposvs  20261  mat1dimelbas  20277  mdetrlin  20408  lmfval  21036  txbasex  21369  txopn  21405  txcn  21429  txrest  21434  txindislem  21436  xkoinjcn  21490  tsmsxp  21958  ustssel  22009  ustfilxp  22016  trust  22033  restutop  22041  trcfilu  22098  cfiluweak  22099  imasdsf1olem  22178  blfvalps  22188  metustfbas  22362  restmetu  22375  bcthlem1  23121  bcthlem5  23125  rrxip  23178  perpln1  25605  perpln2  25606  isperp  25607  isleag  25733  isvcOLD  27434  resf1o  29505  locfinref  29908  metidval  29933  esum2dlem  30154  esum2d  30155  esumiun  30156  elsx  30257  madeval  31935  filnetlem3  32375  filnetlem4  32376  bj-xpexg2  32947  isrngod  33697  isgrpda  33754  iscringd  33797  inxpex  34107  wdom2d2  37602  unxpwdom3  37665  trclubgNEW  37925  relexpxpnnidm  37995  relexpxpmin  38009  enrelmap  38291  rfovd  38295  rfovcnvf1od  38298  fsovrfovd  38303  xpexd  39285  dvsinax  40127  sge0xp  40646  mpt2exxg2  42116