Definition df-comlaw

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccomlaw	⊢ comLaw
1		vo	⊢ 𝑜
2		vm	⊢ 𝑚
3		vx	⊢ 𝑥
4	2	cv	⊢ 𝑚
5		vy	⊢ 𝑦
6	3	cv	⊢ 𝑥
7	1	cv	⊢ 𝑜
8	5	cv	⊢ 𝑦
9	6 8 7	co	⊢ ( 𝑥 𝑜 𝑦 )
10	8 6 7	co	⊢ ( 𝑦 𝑜 𝑥 )
11	9 10	wceq	⊢ ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 )
12	11 5 4	wral	⊢ ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 )
13	12 3 4	wral	⊢ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 )
14	13 1 2	copab	⊢ { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) }
15	0 14	wceq	⊢ comLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) }