Theorem xpexg

Description: The Cartesian product of two sets is a set. Proposition 6.2 of TakeutiZaring p. 23. See also xpexgALT . (Contributed by NM, 14-Aug-1994)

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

Proof

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