Theorem xpexg 3259

Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23.

Assertion

Ref	Expression
xpexg	|- ((A e. C /\ B e. D) -> (A X. B) e. V)

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		unexg 2874	. . 3 |- ((A e. C /\ B e. D) -> (A u. B) e. V)
2		pwexg 2746	. . 3 |- ((A u. B) e. V -> P~(A u. B) e. V)
3	1, 2	syl 10	. 2 |- ((A e. C /\ B e. D) -> P~(A u. B) e. V)
4		pwexg 2746	. 2 |- (P~(A u. B) e. V -> P~P~(A u. B) e. V)
5		xpsspw 3257	. . 3 |- (A X. B) (_ P~P~(A u. B)
6		ssexg 2721	. . 3 |- (((A X. B) (_ P~P~(A u. B) /\ P~P~(A u. B) e. V) -> (A X. B) e. V)
7	5, 6	mpan 695	. 2 |- (P~P~(A u. B) e. V -> (A X. B) e. V)
8	3, 4, 7	3syl 20	1 |- ((A e. C /\ B e. D) -> (A X. B) e. V)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 958  Vcvv 1811   u. cun 2045   (_ wss 2047  P~cpw 2401   X. cxp 3168

This theorem is referenced by:  xpex 3260  resiexg 3396  cnvexg 3519  coexg 3524  resfunexg 3579  cofunexg 3580  fnex 3607  fabexg 3653  oprabex2g 4020  pmex 4327  mapex 4328  ixpexg 4358  fodomr 4483  cdavalt 4919  lmfval 7925  caufval 7926  lmbr 7928  iscau 7936  isvc 8200

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-opab 2667  df-xp 3184  df-rel 3185

Copyright terms: Public domain