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	$$⊢\mathrm{assIntOp}=\left(m\in \mathrm{V}⟼\left\{o\in \mathrm{clIntOp}\left(m\right)|o\mathrm{assLaw}m\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cassintop	$$class\mathrm{assIntOp}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		vo	$$setvaro$$
4		cclintop	$$class\mathrm{clIntOp}$$
5	1	cv	$$setvarm$$
6	5 4	cfv	$$class\mathrm{clIntOp}\left(m\right)$$
7	3	cv	$$setvaro$$
8		casslaw	$$class\mathrm{assLaw}$$
9	7 5 8	wbr	$$wffo\mathrm{assLaw}m$$
10	9 3 6	crab	$$class\left\{o\in \mathrm{clIntOp}\left(m\right)|o\mathrm{assLaw}m\right\}$$
11	1 2 10	cmpt	$$class\left(m\in \mathrm{V}⟼\left\{o\in \mathrm{clIntOp}\left(m\right)|o\mathrm{assLaw}m\right\}\right)$$
12	0 11	wceq	$$wff\mathrm{assIntOp}=\left(m\in \mathrm{V}⟼\left\{o\in \mathrm{clIntOp}\left(m\right)|o\mathrm{assLaw}m\right\}\right)$$