Theorem xpexg

Description: The Cartesian product of two sets is a set. Proposition 6.2 of TakeutiZaring p. 23. See also xpexgALT . (Contributed by NM, 14-Aug-1994)

	Ref	Expression
Assertion	xpexg	|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )

Proof

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