Metamath Proof Explorer


Theorem tlmtps

Description: A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion tlmtps
|- ( W e. TopMod -> W e. TopSp )

Proof

Step Hyp Ref Expression
1 tlmtmd
 |-  ( W e. TopMod -> W e. TopMnd )
2 tmdtps
 |-  ( W e. TopMnd -> W e. TopSp )
3 1 2 syl
 |-  ( W e. TopMod -> W e. TopSp )