Definition df-submgm

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)

	Ref	Expression
Assertion	df-submgm	$$⊢\mathrm{SubMgm}=\left(s\in \mathrm{Mgm}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\forall x\in t\forall y\in tx{+}_{s}y\in t\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubmgm	$$class\mathrm{SubMgm}$$
1		vs	$$setvars$$
2		cmgm	$$class\mathrm{Mgm}$$
3		vt	$$setvart$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvars$$
6	5 4	cfv	$$class{\mathrm{Base}}_s$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_s$$
8		vx	$$setvarx$$
9	3	cv	$$setvart$$
10		vy	$$setvary$$
11	8	cv	$$setvarx$$
12		cplusg	$$class{+}_{𝑔}$$
13	5 12	cfv	$$class{+}_s$$
14	10	cv	$$setvary$$
15	11 14 13	co	$$class\left(x{+}_{s}y\right)$$
16	15 9	wcel	$$wffx{+}_{s}y\in t$$
17	16 10 9	wral	$$wff\forall y\in tx{+}_{s}y\in t$$
18	17 8 9	wral	$$wff\forall x\in t\forall y\in tx{+}_{s}y\in t$$
19	18 3 7	crab	$$class\left\{t\in 𝒫{\mathrm{Base}}_s|\forall x\in t\forall y\in tx{+}_{s}y\in t\right\}$$
20	1 2 19	cmpt	$$class\left(s\in \mathrm{Mgm}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\forall x\in t\forall y\in tx{+}_{s}y\in t\right\}\right)$$
21	0 20	wceq	$$wff\mathrm{SubMgm}=\left(s\in \mathrm{Mgm}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\forall x\in t\forall y\in tx{+}_{s}y\in t\right\}\right)$$