Metamath Proof Explorer


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 𝐽 = ( TopOpen ‘ 𝐺 )
tgptopon.x 𝑋 = ( Base ‘ 𝐺 )
Assertion tgptopon ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgptopon.x 𝑋 = ( Base ‘ 𝐺 )
3 tgptps ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )
4 2 1 istps ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 3 4 sylib ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )