Definition df-assintop 41837

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

Assertion

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

Distinct variable group:   m, o

Detailed syntax breakdown of Definition df-assintop

Step	Hyp	Ref	Expression
1		cassintop 41834	. 2 class assIntOp
2		vm	. . 3 setvar m
3		cvv 3200	. . 3 class _V
4		vo	. . . . . 6 setvar o
5	4	cv 1482	. . . . 5 class o
6	2	cv 1482	. . . . 5 class m
7		casslaw 41820	. . . . 5 class assLaw
8	5, 6, 7	wbr 4653	. . . 4 wff o assLaw m
9		cclintop 41833	. . . . 5 class clIntOp
10	6, 9	cfv 5888	. . . 4 class ( clIntOp ` m )
11	8, 4, 10	crab 2916	. . 3 class { o e. ( clIntOp ` m ) | o assLaw m }
12	2, 3, 11	cmpt 4729	. 2 class ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )
13	1, 12	wceq 1483	1 wff assIntOp = ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )

This definition is referenced by:  assintopval  41841