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

Definition df-tmd 23927
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 = {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpenβ€˜π‘“) / 𝑗](+π‘“β€˜π‘“) ∈ ((𝑗 Γ—t 𝑗) Cn 𝑗)}
Distinct variable group:   𝑓,𝑗

Detailed syntax breakdown of Definition df-tmd
StepHypRef Expression
1 ctmd 23925 . 2 class TopMnd
2 vf . . . . . . 7 setvar 𝑓
32cv 1532 . . . . . 6 class 𝑓
4 cplusf 18568 . . . . . 6 class +𝑓
53, 4cfv 6536 . . . . 5 class (+π‘“β€˜π‘“)
6 vj . . . . . . . 8 setvar 𝑗
76cv 1532 . . . . . . 7 class 𝑗
8 ctx 23415 . . . . . . 7 class Γ—t
97, 7, 8co 7404 . . . . . 6 class (𝑗 Γ—t 𝑗)
10 ccn 23079 . . . . . 6 class Cn
119, 7, 10co 7404 . . . . 5 class ((𝑗 Γ—t 𝑗) Cn 𝑗)
125, 11wcel 2098 . . . 4 wff (+π‘“β€˜π‘“) ∈ ((𝑗 Γ—t 𝑗) Cn 𝑗)
13 ctopn 17374 . . . . 5 class TopOpen
143, 13cfv 6536 . . . 4 class (TopOpenβ€˜π‘“)
1512, 6, 14wsbc 3772 . . 3 wff [(TopOpenβ€˜π‘“) / 𝑗](+π‘“β€˜π‘“) ∈ ((𝑗 Γ—t 𝑗) Cn 𝑗)
16 cmnd 18665 . . . 4 class Mnd
17 ctps 22785 . . . 4 class TopSp
1816, 17cin 3942 . . 3 class (Mnd ∩ TopSp)
1915, 2, 18crab 3426 . 2 class {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpenβ€˜π‘“) / 𝑗](+π‘“β€˜π‘“) ∈ ((𝑗 Γ—t 𝑗) Cn 𝑗)}
201, 19wceq 1533 1 wff TopMnd = {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpenβ€˜π‘“) / 𝑗](+π‘“β€˜π‘“) ∈ ((𝑗 Γ—t 𝑗) Cn 𝑗)}
Colors of variables: wff setvar class
This definition is referenced by:  istmd  23929
  Copyright terms: Public domain W3C validator