Definition df-mgm

Description: Amagma is a set equipped with an everywhere defined internal operation. Definition 1 in BourbakiAlg1 p. 1, or definition of a groupoid in section I.1 of Bruck p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

	Ref	Expression
Assertion	df-mgm	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm	|- Mgm
1		vg	|- g
2		cbs	|- Base
3	1	cv	|- g
4	3 2	cfv	|- ( Base ` g )
5		vb	|- b
6		cplusg	|- +g
7	3 6	cfv	|- ( +g ` g )
8		vo	|- o
9		vx	|- x
10	5	cv	|- b
11		vy	|- y
12	9	cv	|- x
13	8	cv	|- o
14	11	cv	|- y
15	12 14 13	co	|- ( x o y )
16	15 10	wcel	|- ( x o y ) e. b
17	16 11 10	wral	|- A. y e. b ( x o y ) e. b
18	17 9 10	wral	|- A. x e. b A. y e. b ( x o y ) e. b
19	18 8 7	wsbc	|- [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b
20	19 5 4	wsbc	|- [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b
21	20 1	cab	|- { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
22	0 21	wceq	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }