Metamath Proof Explorer


Theorem tgptmd

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

Ref Expression
Assertion tgptmd ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 eqid ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
2 eqid ( invg𝐺 ) = ( invg𝐺 )
3 1 2 istgp ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ ( invg𝐺 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
4 3 simp2bi ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )