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

Definition df-submnd 17107
Description: A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
Assertion
Ref Expression
df-submnd SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
Distinct variable group:   𝑡,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-submnd
StepHypRef Expression
1 csubmnd 17105 . 2 class SubMnd
2 vs . . 3 setvar 𝑠
3 cmnd 17065 . . 3 class Mnd
42cv 1473 . . . . . . 7 class 𝑠
5 c0g 15871 . . . . . . 7 class 0g
64, 5cfv 5789 . . . . . 6 class (0g𝑠)
7 vt . . . . . . 7 setvar 𝑡
87cv 1473 . . . . . 6 class 𝑡
96, 8wcel 1976 . . . . 5 wff (0g𝑠) ∈ 𝑡
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1473 . . . . . . . . 9 class 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1473 . . . . . . . . 9 class 𝑦
14 cplusg 15716 . . . . . . . . . 10 class +g
154, 14cfv 5789 . . . . . . . . 9 class (+g𝑠)
1611, 13, 15co 6526 . . . . . . . 8 class (𝑥(+g𝑠)𝑦)
1716, 8wcel 1976 . . . . . . 7 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1817, 12, 8wral 2895 . . . . . 6 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1918, 10, 8wral 2895 . . . . 5 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
209, 19wa 382 . . . 4 wff ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)
21 cbs 15643 . . . . . 6 class Base
224, 21cfv 5789 . . . . 5 class (Base‘𝑠)
2322cpw 4107 . . . 4 class 𝒫 (Base‘𝑠)
2420, 7, 23crab 2899 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)}
252, 3, 24cmpt 4637 . 2 class (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
261, 25wceq 1474 1 wff SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
Colors of variables: wff setvar class
This definition is referenced by:  submrcl  17117  issubm  17118
  Copyright terms: Public domain W3C validator