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 \in V ⟼ m intOp m)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclintop	$class clIntOp$
1		vm	$setvar m$
2		cvv	$class V$
3	1	cv	$setvar m$
4		cintop	$class intOp$
5	3 3 4	co	$class (m intOp m)$
6	1 2 5	cmpt	$class (m \in V ⟼ m intOp m)$
7	0 6	wceq	$wff clIntOp = (m \in V ⟼ m intOp m)$