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 41567
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 41565 . 2 class SubMgm
2 vs . . 3 setvar 𝑠
3 cmgm 17004 . . 3 class Mgm
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1473 . . . . . . . 8 class 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1473 . . . . . . . 8 class 𝑦
82cv 1473 . . . . . . . . 9 class 𝑠
9 cplusg 15709 . . . . . . . . 9 class +g
108, 9cfv 5785 . . . . . . . 8 class (+g𝑠)
115, 7, 10co 6522 . . . . . . 7 class (𝑥(+g𝑠)𝑦)
12 vt . . . . . . . 8 setvar 𝑡
1312cv 1473 . . . . . . 7 class 𝑡
1411, 13wcel 1975 . . . . . 6 wff (𝑥(+g𝑠)𝑦) ∈ 𝑡
1514, 6, 13wral 2890 . . . . 5 wff 𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
1615, 4, 13wral 2890 . . . 4 wff 𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡
17 cbs 15636 . . . . . 6 class Base
188, 17cfv 5785 . . . . 5 class (Base‘𝑠)
1918cpw 4102 . . . 4 class 𝒫 (Base‘𝑠)
2016, 12, 19crab 2894 . . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡}
212, 3, 20cmpt 4632 . 2 class (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
221, 21wceq 1474 1 wff SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡})
Colors of variables: wff setvar class
This definition is referenced by:  submgmrcl  41569  issubmgm  41576
  Copyright terms: Public domain W3C validator