Definition df-comlaw 41613

Description: The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative 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 AV, 7-Jan-2020.)

Assertion

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

Distinct variable group:   𝑚,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-comlaw

Step	Hyp	Ref	Expression
1		ccomlaw 41611	. 2 class comLaw
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1474	. . . . . . 7 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1474	. . . . . . 7 class 𝑦
6		vo	. . . . . . . 8 setvar 𝑜
7	6	cv 1474	. . . . . . 7 class 𝑜
8	3, 5, 7	co 6549	. . . . . 6 class (𝑥𝑜𝑦)
9	5, 3, 7	co 6549	. . . . . 6 class (𝑦𝑜𝑥)
10	8, 9	wceq 1475	. . . . 5 wff (𝑥𝑜𝑦) = (𝑦𝑜𝑥)
11		vm	. . . . . 6 setvar 𝑚
12	11	cv 1474	. . . . 5 class 𝑚
13	10, 4, 12	wral 2896	. . . 4 wff ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)
14	13, 2, 12	wral 2896	. . 3 wff ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)
15	14, 6, 11	copab 4642	. 2 class {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)}
16	1, 15	wceq 1475	1 wff comLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)}

This definition is referenced by:  iscomlaw  41616