Metamath Proof Explorer


Theorem tmdtps

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

Ref Expression
Assertion tmdtps ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 eqid ( +𝑓𝐺 ) = ( +𝑓𝐺 )
2 eqid ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
3 1 2 istmd ( 𝐺 ∈ TopMnd ↔ ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ ( +𝑓𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
4 3 simp2bi ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp )