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

Step	Hyp	Ref	Expression
1		csubmgm 45005	. 2 class SubMgm
2		vs	. . 3 setvar 𝑠
3		cmgm 18112	. . 3 class Mgm
4		vx	. . . . . . . . 9 setvar 𝑥
5	4	cv 1542	. . . . . . . 8 class 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1542	. . . . . . . 8 class 𝑦
8	2	cv 1542	. . . . . . . . 9 class 𝑠
9		cplusg 16802	. . . . . . . . 9 class +g
10	8, 9	cfv 6380	. . . . . . . 8 class (+g‘𝑠)
11	5, 7, 10	co 7213	. . . . . . 7 class (𝑥(+g‘𝑠)𝑦)
12		vt	. . . . . . . 8 setvar 𝑡
13	12	cv 1542	. . . . . . 7 class 𝑡
14	11, 13	wcel 2110	. . . . . 6 wff (𝑥(+g‘𝑠)𝑦) ∈ 𝑡
15	14, 6, 13	wral 3061	. . . . 5 wff ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡
16	15, 4, 13	wral 3061	. . . 4 wff ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡
17		cbs 16760	. . . . . 6 class Base
18	8, 17	cfv 6380	. . . . 5 class (Base‘𝑠)
19	18	cpw 4513	. . . 4 class 𝒫 (Base‘𝑠)
20	16, 12, 19	crab 3065	. . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡}
21	2, 3, 20	cmpt 5135	. 2 class (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡})
22	1, 21	wceq 1543	1 wff SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡})

This definition is referenced by:  submgmrcl  45009  issubmgm  45016