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	$⊢ SubMnd = (s \in Mnd ⟼ \{t \in 𝒫 {Base}_{s} \| (0_{s} \in t \land \forall x \in t \forall y \in t x +_{s} y \in t)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubmnd	$class SubMnd$
1		vs	$setvar s$
2		cmnd	$class Mnd$
3		vt	$setvar t$
4		cbs	$class Base$
5	1	cv	$setvar s$
6	5 4	cfv	$class {Base}_{s}$
7	6	cpw	$class 𝒫 {Base}_{s}$
8		c0g	$class 0_{𝑔}$
9	5 8	cfv	$class 0_{s}$
10	3	cv	$setvar t$
11	9 10	wcel	$wff 0_{s} \in t$
12		vx	$setvar x$
13		vy	$setvar y$
14	12	cv	$setvar x$
15		cplusg	$class +_{𝑔}$
16	5 15	cfv	$class +_{s}$
17	13	cv	$setvar y$
18	14 17 16	co	$class (x +_{s} y)$
19	18 10	wcel	$wff x +_{s} y \in t$
20	19 13 10	wral	$wff \forall y \in t x +_{s} y \in t$
21	20 12 10	wral	$wff \forall x \in t \forall y \in t x +_{s} y \in t$
22	11 21	wa	$wff (0_{s} \in t \land \forall x \in t \forall y \in t x +_{s} y \in t)$
23	22 3 7	crab	$class \{t \in 𝒫 {Base}_{s} \| (0_{s} \in t \land \forall x \in t \forall y \in t x +_{s} y \in t)\}$
24	1 2 23	cmpt	$class (s \in Mnd ⟼ \{t \in 𝒫 {Base}_{s} \| (0_{s} \in t \land \forall x \in t \forall y \in t x +_{s} y \in t)\})$
25	0 24	wceq	$wff SubMnd = (s \in Mnd ⟼ \{t \in 𝒫 {Base}_{s} \| (0_{s} \in t \land \forall x \in t \forall y \in t x +_{s} y \in t)\})$

Metamath Proof Explorer

Definition df-submnd

Detailed syntax breakdown