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=\mathrm{TopOpen}\left(G\right)$$
	tgpinv.5	$$⊢I={inv}_g\left(G\right)$$
Assertion	tgpinv	$$⊢G\in \mathrm{TopGrp}\to I\in \left(J\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
2		tgpinv.5	$$⊢I={inv}_g\left(G\right)$$
3	1 2	istgp	$$⊢G\in \mathrm{TopGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{TopMnd}\wedge I\in \left(J\mathrm{Cn}J\right)\right)$$
4	3	simp3bi	$$⊢G\in \mathrm{TopGrp}\to I\in \left(J\mathrm{Cn}J\right)$$