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 = ( TopOpen ` G )
	tgptopon.x	|- X = ( Base ` G )
Assertion	tgptopon	|- ( G e. TopGrp -> J e. ( TopOn ` X ) )

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	|- J = ( TopOpen ` G )
2		tgptopon.x	|- X = ( Base ` G )
3		tgptps	|- ( G e. TopGrp -> G e. TopSp )
4	2 1	istps	|- ( G e. TopSp <-> J e. ( TopOn ` X ) )
5	3 4	sylib	|- ( G e. TopGrp -> J e. ( TopOn ` X ) )