Metamath Proof Explorer

Theorem tmdtps

Description: A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Assertion tmdtps ⊢ G ∈ TopMnd → G ∈ TopSp

Proof

Step Hyp Ref Expression
1 eqid ⊢ + 𝑓 ⁡ G = + 𝑓 ⁡ G
2 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
3 1 2 istmd ⊢ G ∈ TopMnd ↔ G ∈ Mnd ∧ G ∈ TopSp ∧ + 𝑓 ⁡ G ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
4 3 simp2bi ⊢ G ∈ TopMnd → G ∈ TopSp