Definition df-mgm 18335

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 = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}

Distinct variable group:   𝑔,𝑏,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-mgm

Step	Hyp	Ref	Expression
1		cmgm 18333	. 2 class Mgm
2		vx	. . . . . . . . . 10 setvar 𝑥
3	2	cv 1538	. . . . . . . . 9 class 𝑥
4		vy	. . . . . . . . . 10 setvar 𝑦
5	4	cv 1538	. . . . . . . . 9 class 𝑦
6		vo	. . . . . . . . . 10 setvar 𝑜
7	6	cv 1538	. . . . . . . . 9 class 𝑜
8	3, 5, 7	co 7284	. . . . . . . 8 class (𝑥𝑜𝑦)
9		vb	. . . . . . . . 9 setvar 𝑏
10	9	cv 1538	. . . . . . . 8 class 𝑏
11	8, 10	wcel 2107	. . . . . . 7 wff (𝑥𝑜𝑦) ∈ 𝑏
12	11, 4, 10	wral 3065	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏
13	12, 2, 10	wral 3065	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏
14		vg	. . . . . . 7 setvar 𝑔
15	14	cv 1538	. . . . . 6 class 𝑔
16		cplusg 16971	. . . . . 6 class +g
17	15, 16	cfv 6437	. . . . 5 class (+g‘𝑔)
18	13, 6, 17	wsbc 3717	. . . 4 wff [(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏
19		cbs 16921	. . . . 5 class Base
20	15, 19	cfv 6437	. . . 4 class (Base‘𝑔)
21	18, 9, 20	wsbc 3717	. . 3 wff [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏
22	21, 14	cab 2716	. 2 class {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
23	1, 22	wceq 1539	1 wff Mgm = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}

This definition is referenced by:  ismgm  18336