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 ) ) |
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 ) ) |