Theorem tgptopon

Description: The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	tgpcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
	tgptopon.x	$$⊢X={\mathrm{Base}}_G$$
Assertion	tgptopon	$$⊢G\in \mathrm{TopGrp}\to J\in \mathrm{TopOn}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
2		tgptopon.x	$$⊢X={\mathrm{Base}}_G$$
3		tgptps	$$⊢G\in \mathrm{TopGrp}\to G\in \mathrm{TopSp}$$
4	2 1	istps	$$⊢G\in \mathrm{TopSp}\leftrightarrow J\in \mathrm{TopOn}\left(X\right)$$
5	3 4	sylib	$$⊢G\in \mathrm{TopGrp}\to J\in \mathrm{TopOn}\left(X\right)$$