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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm	⊢ Mgm
1		vg	⊢ 𝑔
2		cbs	⊢ Base
3	1	cv	⊢ 𝑔
4	3 2	cfv	⊢ ( Base ‘ 𝑔 )
5		vb	⊢ 𝑏
6		cplusg	⊢ +g
7	3 6	cfv	⊢ ( +g ‘ 𝑔 )
8		vo	⊢ 𝑜
9		vx	⊢ 𝑥
10	5	cv	⊢ 𝑏
11		vy	⊢ 𝑦
12	9	cv	⊢ 𝑥
13	8	cv	⊢ 𝑜
14	11	cv	⊢ 𝑦
15	12 14 13	co	⊢ ( 𝑥 𝑜 𝑦 )
16	15 10	wcel	⊢ ( 𝑥 𝑜 𝑦 ) ∈ 𝑏
17	16 11 10	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏
18	17 9 10	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏
19	18 8 7	wsbc	⊢ [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏
20	19 5 4	wsbc	⊢ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏
21	20 1	cab	⊢ { 𝑔 ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 }
22	0 21	wceq	⊢ Mgm = { 𝑔 ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 }