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

Definition df-submnd 17952
 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 17950 . 2 class SubMnd
2 vs . . 3 setvar 𝑠
3 cmnd 17906 . . 3 class Mnd
42cv 1537 . . . . . . 7 class 𝑠
5 c0g 16708 . . . . . . 7 class 0g
64, 5cfv 6325 . . . . . 6 class (0g𝑠)
7 vt . . . . . . 7 setvar 𝑡
87cv 1537 . . . . . 6 class 𝑡
96, 8wcel 2111 . . . . 5 wff (0g𝑠) ∈ 𝑡
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1537 . . . . . . . . 9 class 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1537 . . . . . . . . 9 class 𝑦
14 cplusg 16560 . . . . . . . . . 10 class +g
154, 14cfv 6325 . . . . . . . . 9 class (+g𝑠)
1611, 13, 15co 7136 . . . . . . . 8 class (𝑥(+g𝑠)𝑦)
1716, 8wcel 2111 . . . . . . 7 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1817, 12, 8wral 3106 . . . . . 6 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1918, 10, 8wral 3106 . . . . 5 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
209, 19wa 399 . . . 4 wff ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)
21 cbs 16478 . . . . . 6 class Base
224, 21cfv 6325 . . . . 5 class (Base‘𝑠)
2322cpw 4497 . . . 4 class 𝒫 (Base‘𝑠)
2420, 7, 23crab 3110 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)}
252, 3, 24cmpt 5111 . 2 class (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
261, 25wceq 1538 1 wff SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
 Colors of variables: wff setvar class This definition is referenced by:  submrcl  17962  issubm  17963
 Copyright terms: Public domain W3C validator