Metamath Proof Explorer

Theorem tmdmnd

Description: A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Assertion tmdmnd 
|- ( G e. TopMnd -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( +f ` G ) = ( +f ` G )
2 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
3 1 2 istmd 
 |-  ( G e. TopMnd <-> ( G e. Mnd /\ G e. TopSp /\ ( +f ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) )
4 3 simp1bi 
 |-  ( G e. TopMnd -> G e. Mnd )