Metamath Proof Explorer


Definition df-clintop

Description: Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of Hall p. 2, definition in section I.1 of Bruck p. 1, or definition 1 in BourbakiAlg1 p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion df-clintop
|- clIntOp = ( m e. _V |-> ( m intOp m ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclintop
 |-  clIntOp
1 vm
 |-  m
2 cvv
 |-  _V
3 1 cv
 |-  m
4 cintop
 |-  intOp
5 3 3 4 co
 |-  ( m intOp m )
6 1 2 5 cmpt
 |-  ( m e. _V |-> ( m intOp m ) )
7 0 6 wceq
 |-  clIntOp = ( m e. _V |-> ( m intOp m ) )