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	⊢ SubMnd = ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubmnd	⊢ SubMnd
1		vs	⊢ 𝑠
2		cmnd	⊢ Mnd
3		vt	⊢ 𝑡
4		cbs	⊢ Base
5	1	cv	⊢ 𝑠
6	5 4	cfv	⊢ ( Base ‘ 𝑠 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑠 )
8		c0g	⊢ 0g
9	5 8	cfv	⊢ ( 0g ‘ 𝑠 )
10	3	cv	⊢ 𝑡
11	9 10	wcel	⊢ ( 0g ‘ 𝑠 ) ∈ 𝑡
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14	12	cv	⊢ 𝑥
15		cplusg	⊢ +g
16	5 15	cfv	⊢ ( +g ‘ 𝑠 )
17	13	cv	⊢ 𝑦
18	14 17 16	co	⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 )
19	18 10	wcel	⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡
20	19 13 10	wral	⊢ ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡
21	20 12 10	wral	⊢ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡
22	11 21	wa	⊢ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 )
23	22 3 7	crab	⊢ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) }
24	1 2 23	cmpt	⊢ ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )
25	0 24	wceq	⊢ SubMnd = ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )