ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-submnd GIF version

Definition df-submnd 12714
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 12712 . 2 class SubMnd
2 vs . . 3 setvar 𝑠
3 cmnd 12682 . . 3 class Mnd
42cv 1352 . . . . . . 7 class 𝑠
5 c0g 12626 . . . . . . 7 class 0g
64, 5cfv 5208 . . . . . 6 class (0g𝑠)
7 vt . . . . . . 7 setvar 𝑡
87cv 1352 . . . . . 6 class 𝑡
96, 8wcel 2146 . . . . 5 wff (0g𝑠) ∈ 𝑡
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1352 . . . . . . . . 9 class 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1352 . . . . . . . . 9 class 𝑦
14 cplusg 12492 . . . . . . . . . 10 class +g
154, 14cfv 5208 . . . . . . . . 9 class (+g𝑠)
1611, 13, 15co 5865 . . . . . . . 8 class (𝑥(+g𝑠)𝑦)
1716, 8wcel 2146 . . . . . . 7 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1817, 12, 8wral 2453 . . . . . 6 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1918, 10, 8wral 2453 . . . . 5 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
209, 19wa 104 . . . 4 wff ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)
21 cbs 12428 . . . . . 6 class Base
224, 21cfv 5208 . . . . 5 class (Base‘𝑠)
2322cpw 3572 . . . 4 class 𝒫 (Base‘𝑠)
2420, 7, 23crab 2457 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)}
252, 3, 24cmpt 4059 . 2 class (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
261, 25wceq 1353 1 wff SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
Colors of variables: wff set class
This definition is referenced by:  submrcl  12724  issubm  12725
  Copyright terms: Public domain W3C validator