Definition df-clintop 41836

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.)

Assertion

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

Detailed syntax breakdown of Definition df-clintop

Step	Hyp	Ref	Expression
1		cclintop 41833	. 2 class clIntOp
2		vm	. . 3 setvar m
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . 4 class m
5		cintop 41832	. . . 4 class intOp
6	4, 4, 5	co 6650	. . 3 class ( m intOp m )
7	2, 3, 6	cmpt 4729	. 2 class ( m e. _V |-> ( m intOp m ) )
8	1, 7	wceq 1483	1 wff clIntOp = ( m e. _V |-> ( m intOp m ) )

This definition is referenced by:  clintopval  41840