Definition df-cllaw 45380

Description: The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.)

Assertion

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

Distinct variable group:   𝑚,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-cllaw

Step	Hyp	Ref	Expression
1		ccllaw 45377	. 2 class clLaw
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1538	. . . . . . 7 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1538	. . . . . . 7 class 𝑦
6		vo	. . . . . . . 8 setvar 𝑜
7	6	cv 1538	. . . . . . 7 class 𝑜
8	3, 5, 7	co 7275	. . . . . 6 class (𝑥𝑜𝑦)
9		vm	. . . . . . 7 setvar 𝑚
10	9	cv 1538	. . . . . 6 class 𝑚
11	8, 10	wcel 2106	. . . . 5 wff (𝑥𝑜𝑦) ∈ 𝑚
12	11, 4, 10	wral 3064	. . . 4 wff ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚
13	12, 2, 10	wral 3064	. . 3 wff ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚
14	13, 6, 9	copab 5136	. 2 class {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚}
15	1, 14	wceq 1539	1 wff clLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚}

This definition is referenced by:  iscllaw  45383  clcllaw  45385