This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = inv g ⁡ G
Assertion tgpinv ⊢ G ∈ TopGrp → I ∈ J Cn J

Proof

Step Hyp Ref Expression
1 tgpcn.j ⊢ J = TopOpen ⁡ G
2 tgpinv.5 ⊢ I = inv g ⁡ G
3 1 2 istgp ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ I ∈ J Cn J
4 3 simp3bi ⊢ G ∈ TopGrp → I ∈ J Cn J