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	$$⊢\mathrm{Mgm}=\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in bxoy\in b\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm	$$class\mathrm{Mgm}$$
1		vg	$$setvarg$$
2		cbs	$$class\mathrm{Base}$$
3	1	cv	$$setvarg$$
4	3 2	cfv	$$class{\mathrm{Base}}_g$$
5		vb	$$setvarb$$
6		cplusg	$$class{+}_{𝑔}$$
7	3 6	cfv	$$class{+}_g$$
8		vo	$$setvaro$$
9		vx	$$setvarx$$
10	5	cv	$$setvarb$$
11		vy	$$setvary$$
12	9	cv	$$setvarx$$
13	8	cv	$$setvaro$$
14	11	cv	$$setvary$$
15	12 14 13	co	$$class\left(xoy\right)$$
16	15 10	wcel	$$wffxoy\in b$$
17	16 11 10	wral	$$wff\forall y\in bxoy\in b$$
18	17 9 10	wral	$$wff\forall x\in b\forall y\in bxoy\in b$$
19	18 8 7	wsbc	$$wff\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in bxoy\in b$$
20	19 5 4	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in bxoy\in b$$
21	20 1	cab	$$class\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in bxoy\in b\right\}$$
22	0 21	wceq	$$wff\mathrm{Mgm}=\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in bxoy\in b\right\}$$