Definition df-asslaw 44089

Description: The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)

Assertion

Ref	Expression
df-asslaw	⊢ assLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}

Distinct variable group:   𝑚,𝑜,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-asslaw

Step	Hyp	Ref	Expression
1		casslaw 44085	. 2 class assLaw
2		vx	. . . . . . . . . 10 setvar 𝑥
3	2	cv 1532	. . . . . . . . 9 class 𝑥
4		vy	. . . . . . . . . 10 setvar 𝑦
5	4	cv 1532	. . . . . . . . 9 class 𝑦
6		vo	. . . . . . . . . 10 setvar 𝑜
7	6	cv 1532	. . . . . . . . 9 class 𝑜
8	3, 5, 7	co 7150	. . . . . . . 8 class (𝑥𝑜𝑦)
9		vz	. . . . . . . . 9 setvar 𝑧
10	9	cv 1532	. . . . . . . 8 class 𝑧
11	8, 10, 7	co 7150	. . . . . . 7 class ((𝑥𝑜𝑦)𝑜𝑧)
12	5, 10, 7	co 7150	. . . . . . . 8 class (𝑦𝑜𝑧)
13	3, 12, 7	co 7150	. . . . . . 7 class (𝑥𝑜(𝑦𝑜𝑧))
14	11, 13	wceq 1533	. . . . . 6 wff ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
15		vm	. . . . . . 7 setvar 𝑚
16	15	cv 1532	. . . . . 6 class 𝑚
17	14, 9, 16	wral 3138	. . . . 5 wff ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
18	17, 4, 16	wral 3138	. . . 4 wff ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
19	18, 2, 16	wral 3138	. . 3 wff ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
20	19, 6, 15	copab 5120	. 2 class {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
21	1, 20	wceq 1533	1 wff assLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}

This definition is referenced by:  isasslaw  44093  asslawass  44094