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

Proof

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