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

Detailed syntax breakdown

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