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

Definition df-tmd 20306
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 20304 . 2  class TopMnd
2 vf . . . . . . 7  setvar  f
32cv 1378 . . . . . 6  class  f
4 cplusf 15725 . . . . . 6  class  +f
53, 4cfv 5586 . . . . 5  class  ( +f `  f )
6 vj . . . . . . . 8  setvar  j
76cv 1378 . . . . . . 7  class  j
8 ctx 19796 . . . . . . 7  class  tX
97, 7, 8co 6282 . . . . . 6  class  ( j 
tX  j )
10 ccn 19491 . . . . . 6  class  Cn
119, 7, 10co 6282 . . . . 5  class  ( ( j  tX  j )  Cn  j )
125, 11wcel 1767 . . . 4  wff  ( +f `  f )  e.  ( ( j 
tX  j )  Cn  j )
13 ctopn 14673 . . . . 5  class  TopOpen
143, 13cfv 5586 . . . 4  class  ( TopOpen `  f )
1512, 6, 14wsbc 3331 . . 3  wff  [. ( TopOpen
`  f )  / 
j ]. ( +f `  f )  e.  ( ( j  tX  j
)  Cn  j )
16 cmnd 15722 . . . 4  class  Mnd
17 ctps 19164 . . . 4  class  TopSp
1816, 17cin 3475 . . 3  class  ( Mnd 
i^i  TopSp )
1915, 2, 18crab 2818 . 2  class  { f  e.  ( Mnd  i^i  TopSp
)  |  [. ( TopOpen
`  f )  / 
j ]. ( +f `  f )  e.  ( ( j  tX  j
)  Cn  j ) }
201, 19wceq 1379 1  wff TopMnd  =  {
f  e.  ( Mnd 
i^i  TopSp )  |  [. ( TopOpen `  f )  /  j ]. ( +f `  f
)  e.  ( ( j  tX  j )  Cn  j ) }
Colors of variables: wff setvar class
This definition is referenced by:  istmd  20308
  Copyright terms: Public domain W3C validator