This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tmdtopon

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

Ref Expression
Hypotheses tgpcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tgptopon.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion tmdtopon ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )

Proof

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