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

Definition df-tmd 19618
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 19616 . 2  class TopMnd
2 vf . . . . . . 7  setvar  f
32cv 1368 . . . . . 6  class  f
4 cplusf 15404 . . . . . 6  class  +f
53, 4cfv 5413 . . . . 5  class  ( +f `  f )
6 vj . . . . . . . 8  setvar  j
76cv 1368 . . . . . . 7  class  j
8 ctx 19108 . . . . . . 7  class  tX
97, 7, 8co 6086 . . . . . 6  class  ( j 
tX  j )
10 ccn 18803 . . . . . 6  class  Cn
119, 7, 10co 6086 . . . . 5  class  ( ( j  tX  j )  Cn  j )
125, 11wcel 1756 . . . 4  wff  ( +f `  f )  e.  ( ( j 
tX  j )  Cn  j )
13 ctopn 14352 . . . . 5  class  TopOpen
143, 13cfv 5413 . . . 4  class  ( TopOpen `  f )
1512, 6, 14wsbc 3181 . . 3  wff  [. ( TopOpen
`  f )  / 
j ]. ( +f `  f )  e.  ( ( j  tX  j
)  Cn  j )
16 cmnd 15401 . . . 4  class  Mnd
17 ctps 18476 . . . 4  class  TopSp
1816, 17cin 3322 . . 3  class  ( Mnd 
i^i  TopSp )
1915, 2, 18crab 2714 . 2  class  { f  e.  ( Mnd  i^i  TopSp
)  |  [. ( TopOpen
`  f )  / 
j ]. ( +f `  f )  e.  ( ( j  tX  j
)  Cn  j ) }
201, 19wceq 1369 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  19620
  Copyright terms: Public domain W3C validator