Theorem xpexg 4774

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 4772	. 2 |- ( A X. B ) C_ ~P ~P ( A u. B )
2		unexg 4475	. . 3 |- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
3		pwexg 4210	. . 3 |- ( ( A u. B ) e. _V -> ~P ( A u. B ) e. _V )
4		pwexg 4210	. . 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 4169	. 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 2164   _Vcvv 2760   u. cun 3152   C_ wss 3154   ~Pcpw 3602   X. cxp 4658

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 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-opab 4092  df-xp 4666

This theorem is referenced by:  xpex  4775  sqxpexg  4776  resiexg  4988  cnvexg  5204  coexg  5211  fex2  5423  fabexg  5442  resfunexgALT  6162  cofunexg  6163  fnexALT  6165  funexw  6166  opabex3d  6175  opabex3  6176  oprabexd  6181  ofmresex  6191  mpoexxg  6265  tposexg  6313  erex  6613  pmex  6709  mapex  6710  pmvalg  6715  elpmg  6720  fvdiagfn  6749  ixpexgg  6778  ixpsnf1o  6792  map1  6868  xpdom2  6887  xpdom3m  6890  xpen  6903  mapxpen  6906  xpfi  6988  djuex  7104  djuassen  7279  cc2lem  7328  shftfvalg  10965  climconst2  11437  mulgnngsum  13200  releqgg  13293  eqgex  13294  eqgfval  13295  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrex  13597  aprval  13781  aprap  13785  psrval  14163  psrbasg  14170  psrplusgg  14173  lmfval  14371  txbasex  14436  txopn  14444  txcn  14454  txrest  14455  blfvalps  14564  xmetxp  14686  limccnp2lem  14855  limccnp2cntop  14856  dvfvalap  14860