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 = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubmgm	|- SubMgm
1		vs	|- s
2		cmgm	|- Mgm
3		vt	|- t
4		cbs	|- Base
5	1	cv	|- s
6	5 4	cfv	|- ( Base ` s )
7	6	cpw	|- ~P ( Base ` s )
8		vx	|- x
9	3	cv	|- t
10		vy	|- y
11	8	cv	|- x
12		cplusg	|- +g
13	5 12	cfv	|- ( +g ` s )
14	10	cv	|- y
15	11 14 13	co	|- ( x ( +g ` s ) y )
16	15 9	wcel	|- ( x ( +g ` s ) y ) e. t
17	16 10 9	wral	|- A. y e. t ( x ( +g ` s ) y ) e. t
18	17 8 9	wral	|- A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t
19	18 3 7	crab	|- { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t }
20	1 2 19	cmpt	|- ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )
21	0 20	wceq	|- SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )