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 e. TopGrp -> G e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
2 eqid 
 |-  ( invg ` G ) = ( invg ` G )
3 1 2 istgp 
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) ) )
4 3 simp1bi 
 |-  ( G e. TopGrp -> G e. Grp )