Metamath Proof Explorer

Theorem tgptmd

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

Ref Expression
Assertion tgptmd ⊢G∈TopGrp→G∈TopMnd

Proof

Step Hyp Ref Expression
1 eqid ⊢TopOpen⁡G=TopOpen⁡G
2 eqid ⊢invg⁡G=invg⁡G
3 1 2 istgp ⊢G∈TopGrp↔G∈Grp∧G∈TopMnd∧invg⁡G∈TopOpen⁡GCnTopOpen⁡G
4 3 simp2bi ⊢G∈TopGrp→G∈TopMnd