Theorem tmdmnd

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

	Ref	Expression
Assertion	tmdmnd	$$⊢G\in \mathrm{TopMnd}\to G\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{+}_{𝑓}\left(G\right)={+}_{𝑓}\left(G\right)$$
2		eqid	$$⊢\mathrm{TopOpen}\left(G\right)=\mathrm{TopOpen}\left(G\right)$$
3	1 2	istmd	$$⊢G\in \mathrm{TopMnd}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge G\in \mathrm{TopSp}\wedge {+}_{𝑓}\left(G\right)\in \left(\left(\mathrm{TopOpen}\left(G\right){\times }_t\mathrm{TopOpen}\left(G\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left(G\right)\right)\right)$$
4	3	simp1bi	$$⊢G\in \mathrm{TopMnd}\to G\in \mathrm{Mnd}$$