Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tmd Structured version   Unicode version

Definition df-tmd 18094
 Description: Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
Assertion
Ref Expression
df-tmd TopMnd
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-tmd
StepHypRef Expression
1 ctmd 18092 . 2 TopMnd
2 vf . . . . . . 7
32cv 1651 . . . . . 6
4 cplusf 14679 . . . . . 6
53, 4cfv 5446 . . . . 5
6 vj . . . . . . . 8
76cv 1651 . . . . . . 7
8 ctx 17584 . . . . . . 7
97, 7, 8co 6073 . . . . . 6
10 ccn 17280 . . . . . 6
119, 7, 10co 6073 . . . . 5
125, 11wcel 1725 . . . 4
13 ctopn 13641 . . . . 5
143, 13cfv 5446 . . . 4
1512, 6, 14wsbc 3153 . . 3
16 cmnd 14676 . . . 4
17 ctps 16953 . . . 4
1816, 17cin 3311 . . 3
1915, 2, 18crab 2701 . 2
201, 19wceq 1652 1 TopMnd
 Colors of variables: wff set class This definition is referenced by:  istmd  18096
 Copyright terms: Public domain W3C validator