Theorem tmdmnd

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

	Ref	Expression
Assertion	tmdmnd	⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ Mnd )

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	simp1bi	⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ Mnd )