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