Metamath Proof Explorer

Theorem tgpgrp

Description: A topological group is a group. (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion tgpgrp ⊢ G ∈ TopGrp → G ∈ Grp

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
2 eqid ⊢ inv g ⁡ G = inv g ⁡ G
3 1 2 istgp ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ inv g ⁡ G ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
4 3 simp1bi ⊢ G ∈ TopGrp → G ∈ Grp