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