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 V B W A ×× B V

Proof

Step Hyp Ref Expression
1 altxpsspw A ×× B 𝒫 𝒫 A 𝒫 B
2 pwexg B W 𝒫 B V
3 unexg A V 𝒫 B V A 𝒫 B V
4 2 3 sylan2 A V B W A 𝒫 B V
5 pwexg A 𝒫 B V 𝒫 A 𝒫 B V
6 pwexg 𝒫 A 𝒫 B V 𝒫 𝒫 A 𝒫 B V
7 4 5 6 3syl A V B W 𝒫 𝒫 A 𝒫 B V
8 ssexg A ×× B 𝒫 𝒫 A 𝒫 B 𝒫 𝒫 A 𝒫 B V A ×× B V
9 1 7 8 sylancr A V B W A ×× B V