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 42298
 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 42296 . 2 class SubMgm
2 vs . . 3 setvar 𝑠
3 cmgm 17447 . . 3 class Mgm
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1629 . . . . . . . 8 class 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1629 . . . . . . . 8 class 𝑦
82cv 1629 . . . . . . . . 9 class 𝑠
9 cplusg 16148 . . . . . . . . 9 class +g
108, 9cfv 6031 . . . . . . . 8 class (+g𝑠)
115, 7, 10co 6792 . . . . . . 7 class (𝑥(+g𝑠)𝑦)
12 vt . . . . . . . 8 setvar 𝑡
1312cv 1629 . . . . . . 7 class 𝑡
1411, 13wcel 2144 . . . . . 6 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1514, 6, 13wral 3060 . . . . 5 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1615, 4, 13wral 3060 . . . 4 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
17 cbs 16063 . . . . . 6 class Base
188, 17cfv 6031 . . . . 5 class (Base‘𝑠)
1918cpw 4295 . . . 4 class 𝒫 (Base‘𝑠)
2016, 12, 19crab 3064 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡}
212, 3, 20cmpt 4861 . 2 class (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
221, 21wceq 1630 1 wff SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
 Colors of variables: wff setvar class This definition is referenced by:  submgmrcl  42300  issubmgm  42307
 Copyright terms: Public domain W3C validator