Theorem xpexg 4765

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

Step	Hyp	Ref	Expression
1		xpsspw 4763	. 2 |- ( A X. B ) C_ ~P ~P ( A u. B )
2		unexg 4468	. . 3 |- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
3		pwexg 4205	. . 3 |- ( ( A u. B ) e. _V -> ~P ( A u. B ) e. _V )
4		pwexg 4205	. . 3 |- ( ~P ( A u. B ) e. _V -> ~P ~P ( A u. B ) e. _V )
5	2, 3, 4	3syl 17	. 2 |- ( ( A e. V /\ B e. W ) -> ~P ~P ( A u. B ) e. _V )
6		ssexg 4164	. 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 414	1 |- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2160   _Vcvv 2756   u. cun 3146   C_ wss 3148   ~Pcpw 3597   X. cxp 4649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4143  ax-pow 4199  ax-pr 4234  ax-un 4458

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2758  df-un 3152  df-in 3154  df-ss 3161  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-opab 4087  df-xp 4657

This theorem is referenced by:  xpex  4766  sqxpexg  4767  resiexg  4977  cnvexg  5191  coexg  5198  fex2  5410  fabexg  5429  resfunexgALT  6141  cofunexg  6142  fnexALT  6144  funexw  6145  opabex3d  6154  opabex3  6155  oprabexd  6160  ofmresex  6170  mpoexxg  6243  tposexg  6291  erex  6591  pmex  6687  mapex  6688  pmvalg  6693  elpmg  6698  fvdiagfn  6727  ixpexgg  6756  ixpsnf1o  6770  map1  6846  xpdom2  6865  xpdom3m  6868  xpen  6881  mapxpen  6884  xpfi  6966  djuex  7081  djuassen  7256  cc2lem  7305  shftfvalg  10874  climconst2  11346  mulgnngsum  13100  releqgg  13192  eqgex  13193  eqgfval  13194  reldvdsrsrg  13479  dvdsrvald  13480  dvdsrex  13485  aprval  13641  aprap  13645  psrval  14005  psrbasg  14012  psrplusgg  14015  lmfval  14213  txbasex  14278  txopn  14286  txcn  14296  txrest  14297  blfvalps  14406  xmetxp  14528  limccnp2lem  14683  limccnp2cntop  14684  dvfvalap  14688