Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-submgm Structured version   Visualization version   GIF version

Definition df-submgm 42305
Description: A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020.)
Assertion
Ref Expression
df-submgm SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
Distinct variable group:   𝑡,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-submgm
StepHypRef Expression
1 csubmgm 42303 . 2 class SubMgm
2 vs . . 3 setvar 𝑠
3 cmgm 17448 . . 3 class Mgm
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1630 . . . . . . . 8 class 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1630 . . . . . . . 8 class 𝑦
82cv 1630 . . . . . . . . 9 class 𝑠
9 cplusg 16149 . . . . . . . . 9 class +g
108, 9cfv 6030 . . . . . . . 8 class (+g𝑠)
115, 7, 10co 6796 . . . . . . 7 class (𝑥(+g𝑠)𝑦)
12 vt . . . . . . . 8 setvar 𝑡
1312cv 1630 . . . . . . 7 class 𝑡
1411, 13wcel 2145 . . . . . 6 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1514, 6, 13wral 3061 . . . . 5 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1615, 4, 13wral 3061 . . . 4 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
17 cbs 16064 . . . . . 6 class Base
188, 17cfv 6030 . . . . 5 class (Base‘𝑠)
1918cpw 4298 . . . 4 class 𝒫 (Base‘𝑠)
2016, 12, 19crab 3065 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡}
212, 3, 20cmpt 4864 . 2 class (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
221, 21wceq 1631 1 wff SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
Colors of variables: wff setvar class
This definition is referenced by:  submgmrcl  42307  issubmgm  42314
  Copyright terms: Public domain W3C validator