Theorem tmdtps

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

	Ref	Expression
Assertion	tmdtps	$$⊢G\in \mathrm{TopMnd}\to G\in \mathrm{TopSp}$$

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	simp2bi	$$⊢G\in \mathrm{TopMnd}\to G\in \mathrm{TopSp}$$