Definition df-submgm 45222

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 45220	. 2 class SubMgm
2		vs	. . 3 setvar 𝑠
3		cmgm 18239	. . 3 class Mgm
4		vx	. . . . . . . . 9 setvar 𝑥
5	4	cv 1538	. . . . . . . 8 class 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1538	. . . . . . . 8 class 𝑦
8	2	cv 1538	. . . . . . . . 9 class 𝑠
9		cplusg 16888	. . . . . . . . 9 class +g
10	8, 9	cfv 6418	. . . . . . . 8 class (+g‘𝑠)
11	5, 7, 10	co 7255	. . . . . . 7 class (𝑥(+g‘𝑠)𝑦)
12		vt	. . . . . . . 8 setvar 𝑡
13	12	cv 1538	. . . . . . 7 class 𝑡
14	11, 13	wcel 2108	. . . . . 6 wff (𝑥(+g‘𝑠)𝑦) ∈ 𝑡
15	14, 6, 13	wral 3063	. . . . 5 wff ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡
16	15, 4, 13	wral 3063	. . . 4 wff ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡
17		cbs 16840	. . . . . 6 class Base
18	8, 17	cfv 6418	. . . . 5 class (Base‘𝑠)
19	18	cpw 4530	. . . 4 class 𝒫 (Base‘𝑠)
20	16, 12, 19	crab 3067	. . 3 class {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡}
21	2, 3, 20	cmpt 5153	. 2 class (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡})
22	1, 21	wceq 1539	1 wff SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡})

This definition is referenced by:  submgmrcl  45224  issubmgm  45231