Description: The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | altxpexg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | altxpsspw | ||
2 | pwexg | ||
3 | unexg | ||
4 | 2 3 | sylan2 | |
5 | pwexg | ||
6 | pwexg | ||
7 | 4 5 6 | 3syl | |
8 | ssexg | ||
9 | 1 7 8 | sylancr |