Theorem txuni

Description: The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	txuni.1	⊢ 𝑋 = ∪ 𝑅
	txuni.2	⊢ 𝑌 = ∪ 𝑆
Assertion	txuni	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		txuni.1	⊢ 𝑋 = ∪ 𝑅
2		txuni.2	⊢ 𝑌 = ∪ 𝑆
3	1	toptopon	⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
4	2	toptopon	⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
5		txtopon	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
6	3 4 5	syl2anb	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
7		toponuni	⊢ ( ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
8	6 7	syl	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )