Theorem txunii

Description: The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	txunii.1	⊢ 𝑅 ∈ Top
	txunii.2	⊢ 𝑆 ∈ Top
	txunii.3	⊢ 𝑋 = ∪ 𝑅
	txunii.4	⊢ 𝑌 = ∪ 𝑆
Assertion	txunii	⊢ ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		txunii.1	⊢ 𝑅 ∈ Top
2		txunii.2	⊢ 𝑆 ∈ Top
3		txunii.3	⊢ 𝑋 = ∪ 𝑅
4		txunii.4	⊢ 𝑌 = ∪ 𝑆
5	3 4	txuni	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
6	1 2 5	mp2an	⊢ ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 )