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 = { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccllaw
 |-  clLaw
1 vo
 |-  o
2 vm
 |-  m
3 vx
 |-  x
4 2 cv
 |-  m
5 vy
 |-  y
6 3 cv
 |-  x
7 1 cv
 |-  o
8 5 cv
 |-  y
9 6 8 7 co
 |-  ( x o y )
10 9 4 wcel
 |-  ( x o y ) e. m
11 10 5 4 wral
 |-  A. y e. m ( x o y ) e. m
12 11 3 4 wral
 |-  A. x e. m A. y e. m ( x o y ) e. m
13 12 1 2 copab
 |-  { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }
14 0 13 wceq
 |-  clLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }