Theorem txtopi

Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	txtopi.1	⊢ 𝑅 ∈ Top
	txtopi.2	⊢ 𝑆 ∈ Top
Assertion	txtopi	⊢ ( 𝑅 ×t 𝑆 ) ∈ Top

Proof

Step	Hyp	Ref	Expression
1		txtopi.1	⊢ 𝑅 ∈ Top
2		txtopi.2	⊢ 𝑆 ∈ Top
3		txtop	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
4	1 2 3	mp2an	⊢ ( 𝑅 ×t 𝑆 ) ∈ Top