Definition df-submnd

Description: A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Assertion	df-submnd	$$⊢\mathrm{SubMnd}=\left(s\in \mathrm{Mnd}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\left(0_s\in t\wedge \forall x\in t\forall y\in tx{+}_{s}y\in t\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubmnd	$$class\mathrm{SubMnd}$$
1		vs	$$setvars$$
2		cmnd	$$class\mathrm{Mnd}$$
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		c0g	$$class{0}_{𝑔}$$
9	5 8	cfv	$$class{0}_s$$
10	3	cv	$$setvart$$
11	9 10	wcel	$$wff{0}_s\in t$$
12		vx	$$setvarx$$
13		vy	$$setvary$$
14	12	cv	$$setvarx$$
15		cplusg	$$class{+}_{𝑔}$$
16	5 15	cfv	$$class{+}_s$$
17	13	cv	$$setvary$$
18	14 17 16	co	$$class\left(x{+}_{s}y\right)$$
19	18 10	wcel	$$wffx{+}_{s}y\in t$$
20	19 13 10	wral	$$wff\forall y\in tx{+}_{s}y\in t$$
21	20 12 10	wral	$$wff\forall x\in t\forall y\in tx{+}_{s}y\in t$$
22	11 21	wa	$$wff\left(0_s\in t\wedge \forall x\in t\forall y\in tx{+}_{s}y\in t\right)$$
23	22 3 7	crab	$$class\left\{t\in 𝒫{\mathrm{Base}}_s|\left(0_s\in t\wedge \forall x\in t\forall y\in tx{+}_{s}y\in t\right)\right\}$$
24	1 2 23	cmpt	$$class\left(s\in \mathrm{Mnd}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\left(0_s\in t\wedge \forall x\in t\forall y\in tx{+}_{s}y\in t\right)\right\}\right)$$
25	0 24	wceq	$$wff\mathrm{SubMnd}=\left(s\in \mathrm{Mnd}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\left(0_s\in t\wedge \forall x\in t\forall y\in tx{+}_{s}y\in t\right)\right\}\right)$$