Definition df-mgm 12587

Description: A magma 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.)

Assertion

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

Distinct variable group:   g, b, o, x, y

Detailed syntax breakdown of Definition df-mgm

Step	Hyp	Ref	Expression
1		cmgm 12585	. 2 class Mgm
2		vx	. . . . . . . . . 10 setvar x
3	2	cv 1342	. . . . . . . . 9 class x
4		vy	. . . . . . . . . 10 setvar y
5	4	cv 1342	. . . . . . . . 9 class y
6		vo	. . . . . . . . . 10 setvar o
7	6	cv 1342	. . . . . . . . 9 class o
8	3, 5, 7	co 5842	. . . . . . . 8 class ( x o y )
9		vb	. . . . . . . . 9 setvar b
10	9	cv 1342	. . . . . . . 8 class b
11	8, 10	wcel 2136	. . . . . . 7 wff ( x o y ) e. b
12	11, 4, 10	wral 2444	. . . . . 6 wff A. y e. b ( x o y ) e. b
13	12, 2, 10	wral 2444	. . . . 5 wff A. x e. b A. y e. b ( x o y ) e. b
14		vg	. . . . . . 7 setvar g
15	14	cv 1342	. . . . . 6 class g
16		cplusg 12457	. . . . . 6 class +g
17	15, 16	cfv 5188	. . . . 5 class ( +g ` g )
18	13, 6, 17	wsbc 2951	. . . 4 wff [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b
19		cbs 12394	. . . . 5 class Base
20	15, 19	cfv 5188	. . . 4 class ( Base ` g )
21	18, 9, 20	wsbc 2951	. . 3 wff [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b
22	21, 14	cab 2151	. 2 class { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
23	1, 22	wceq 1343	1 wff Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }

This definition is referenced by:  ismgm  12588