Metamath Proof Explorer

Theorem tgpinv

Description: In a topological group, the inverse function is continuous. (Contributed by FL, 21-Jun-2010) (Revised by FL, 27-Jun-2014)

Ref Expression
Hypotheses tgpcn.j 
|- J = ( TopOpen ` G )
tgpinv.5 
|- I = ( invg ` G )
Assertion tgpinv 
|- ( G e. TopGrp -> I e. ( J Cn J ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j 
 |-  J = ( TopOpen ` G )
2 tgpinv.5 
 |-  I = ( invg ` G )
3 1 2 istgp 
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ I e. ( J Cn J ) ) )
4 3 simp3bi 
 |-  ( G e. TopGrp -> I e. ( J Cn J ) )