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 𝐽 ) )