Theorem altxpexg

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

	Ref	Expression
Assertion	altxpexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ×× 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		altxpsspw	⊢ ( 𝐴 ×× 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 )
2		pwexg	⊢ ( 𝐵 ∈ 𝑊 → 𝒫 𝐵 ∈ V )
3		unexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐵 ∈ V ) → ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V )
4	2 3	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V )
5		pwexg	⊢ ( ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V → 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V )
6		pwexg	⊢ ( 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V → 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V )
7	4 5 6	3syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V )
8		ssexg	⊢ ( ( ( 𝐴 ×× 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ∈ V ) → ( 𝐴 ×× 𝐵 ) ∈ V )
9	1 7 8	sylancr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ×× 𝐵 ) ∈ V )