Metamath Proof Explorer


Definition df-cllaw

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccllaw clLaw
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 9 4 wcel ( 𝑥 𝑜 𝑦 ) ∈ 𝑚
11 10 5 4 wral 𝑦𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚
12 11 3 4 wral 𝑥𝑚𝑦𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚
13 12 1 2 copab { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥𝑚𝑦𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 }
14 0 13 wceq clLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥𝑚𝑦𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 }