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

Definition df-tmd 17755
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  =  {
f  e.  ( Mnd 
i^i  TopSp )  |  [. ( TopOpen `  f )  /  j ]. ( + f `  f )  e.  ( ( j 
tX  j )  Cn  j ) }
Distinct variable group:    f, j

Detailed syntax breakdown of Definition df-tmd
StepHypRef Expression
1 ctmd 17753 . 2  class TopMnd
2 vf . . . . . . 7  set  f
32cv 1622 . . . . . 6  class  f
4 cplusf 14364 . . . . . 6  class  + f
53, 4cfv 5255 . . . . 5  class  ( + f `  f )
6 vj . . . . . . . 8  set  j
76cv 1622 . . . . . . 7  class  j
8 ctx 17255 . . . . . . 7  class  tX
97, 7, 8co 5858 . . . . . 6  class  ( j 
tX  j )
10 ccn 16954 . . . . . 6  class  Cn
119, 7, 10co 5858 . . . . 5  class  ( ( j  tX  j )  Cn  j )
125, 11wcel 1684 . . . 4  wff  ( + f `  f )  e.  ( ( j 
tX  j )  Cn  j )
13 ctopn 13326 . . . . 5  class  TopOpen
143, 13cfv 5255 . . . 4  class  ( TopOpen `  f )
1512, 6, 14wsbc 2991 . . 3  wff  [. ( TopOpen
`  f )  / 
j ]. ( + f `  f )  e.  ( ( j  tX  j
)  Cn  j )
16 cmnd 14361 . . . 4  class  Mnd
17 ctps 16634 . . . 4  class  TopSp
1816, 17cin 3151 . . 3  class  ( Mnd 
i^i  TopSp )
1915, 2, 18crab 2547 . 2  class  { f  e.  ( Mnd  i^i  TopSp
)  |  [. ( TopOpen
`  f )  / 
j ]. ( + f `  f )  e.  ( ( j  tX  j
)  Cn  j ) }
201, 19wceq 1623 1  wff TopMnd  =  {
f  e.  ( Mnd 
i^i  TopSp )  |  [. ( TopOpen `  f )  /  j ]. ( + f `  f )  e.  ( ( j 
tX  j )  Cn  j ) }
Colors of variables: wff set class
This definition is referenced by:  istmd  17757
  Copyright terms: Public domain W3C validator