Definition df-clintop 45282

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 = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))

Detailed syntax breakdown of Definition df-clintop

Step	Hyp	Ref	Expression
1		cclintop 45279	. 2 class clIntOp
2		vm	. . 3 setvar 𝑚
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . 4 class 𝑚
5		cintop 45278	. . . 4 class intOp
6	4, 4, 5	co 7255	. . 3 class (𝑚 intOp 𝑚)
7	2, 3, 6	cmpt 5153	. 2 class (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))
8	1, 7	wceq 1539	1 wff clIntOp = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))

This definition is referenced by:  clintopval  45286