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 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tgpinv.5 ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion tgpinv ( 𝐺 ∈ TopGrp → 𝐼 ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgpinv.5 ⊢ 𝐼 = ( invg ‘ 𝐺 )
3 1 2 istgp ⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
4 3 simp3bi ⊢ ( 𝐺 ∈ TopGrp → 𝐼 ∈ ( 𝐽 Cn 𝐽 ) )