Metamath Proof Explorer

Theorem altxpexg

Description: The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012)

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

Proof

Step Hyp Ref Expression
1 altxpsspw 
 |-  ( A XX. B ) C_ ~P ~P ( A u. ~P B )
2 pwexg 
 |-  ( B e. W -> ~P B e. _V )
3 unexg 
 |-  ( ( A e. V /\ ~P B e. _V ) -> ( A u. ~P B ) e. _V )
4 2 3 sylan2 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. ~P B ) e. _V )
5 pwexg 
 |-  ( ( A u. ~P B ) e. _V -> ~P ( A u. ~P B ) e. _V )
6 pwexg 
 |-  ( ~P ( A u. ~P B ) e. _V -> ~P ~P ( A u. ~P B ) e. _V )
7 4 5 6 3syl 
 |-  ( ( A e. V /\ B e. W ) -> ~P ~P ( A u. ~P B ) e. _V )
8 ssexg 
 |-  ( ( ( A XX. B ) C_ ~P ~P ( A u. ~P B ) /\ ~P ~P ( A u. ~P B ) e. _V ) -> ( A XX. B ) e. _V )
9 1 7 8 sylancr 
 |-  ( ( A e. V /\ B e. W ) -> ( A XX. B ) e. _V )