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 45007
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 45005 . 2 class SubMgm
2 vs . . 3 setvar 𝑠
3 cmgm 18112 . . 3 class Mgm
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1542 . . . . . . . 8 class 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1542 . . . . . . . 8 class 𝑦
82cv 1542 . . . . . . . . 9 class 𝑠
9 cplusg 16802 . . . . . . . . 9 class +g
108, 9cfv 6380 . . . . . . . 8 class (+g𝑠)
115, 7, 10co 7213 . . . . . . 7 class (𝑥(+g𝑠)𝑦)
12 vt . . . . . . . 8 setvar 𝑡
1312cv 1542 . . . . . . 7 class 𝑡
1411, 13wcel 2110 . . . . . 6 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1514, 6, 13wral 3061 . . . . 5 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1615, 4, 13wral 3061 . . . 4 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
17 cbs 16760 . . . . . 6 class Base
188, 17cfv 6380 . . . . 5 class (Base‘𝑠)
1918cpw 4513 . . . 4 class 𝒫 (Base‘𝑠)
2016, 12, 19crab 3065 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡}
212, 3, 20cmpt 5135 . 2 class (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
221, 21wceq 1543 1 wff SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
Colors of variables: wff setvar class
This definition is referenced by:  submgmrcl  45009  issubmgm  45016
  Copyright terms: Public domain W3C validator