Definition df-assintop

Description: Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in BourbakiAlg1 p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	df-assintop	|- assIntOp = ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cassintop	|- assIntOp
1		vm	|- m
2		cvv	|- _V
3		vo	|- o
4		cclintop	|- clIntOp
5	1	cv	|- m
6	5 4	cfv	|- ( clIntOp ` m )
7	3	cv	|- o
8		casslaw	|- assLaw
9	7 5 8	wbr	|- o assLaw m
10	9 3 6	crab	|- { o e. ( clIntOp ` m ) | o assLaw m }
11	1 2 10	cmpt	|- ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )
12	0 11	wceq	|- assIntOp = ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )