Theorem xpexg 4788

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 4786	. 2 |- ( A X. B ) C_ ~P ~P ( A u. B )
2		unexg 4489	. . 3 |- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
3		pwexg 4223	. . 3 |- ( ( A u. B ) e. _V -> ~P ( A u. B ) e. _V )
4		pwexg 4223	. . 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 4182	. 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 2175   _Vcvv 2771   u. cun 3163   C_ wss 3165   ~Pcpw 3615   X. cxp 4672

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-opab 4105  df-xp 4680

This theorem is referenced by:  xpex  4789  sqxpexg  4790  resiexg  5003  cnvexg  5219  coexg  5226  fex2  5443  fabexg  5462  resfunexgALT  6192  cofunexg  6193  fnexALT  6195  funexw  6196  opabex3d  6205  opabex3  6206  oprabexd  6211  ofmresex  6221  mpoexxg  6295  tposexg  6343  erex  6643  pmex  6739  mapex  6740  pmvalg  6745  elpmg  6750  fvdiagfn  6779  ixpexgg  6808  ixpsnf1o  6822  map1  6903  xpdom2  6925  xpdom3m  6928  xpen  6941  mapxpen  6944  xpfi  7028  djuex  7144  djuassen  7328  cc2lem  7377  shftfvalg  11100  climconst2  11573  prdsval  13076  prdsbaslemss  13077  pwsval  13094  pwsbas  13095  mulgnngsum  13434  releqgg  13527  eqgex  13528  eqgfval  13529  reldvdsrsrg  13825  dvdsrvald  13826  dvdsrex  13831  aprval  14015  aprap  14019  psrval  14399  psrbasg  14407  psrplusgg  14411  lmfval  14635  txbasex  14700  txopn  14708  txcn  14718  txrest  14719  blfvalps  14828  xmetxp  14950  limccnp2lem  15119  limccnp2cntop  15120  dvfvalap  15124