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 = ( 𝑚 ∈ V ↦ { 𝑜 ∈ ( clIntOp ‘ 𝑚 ) ∣ 𝑜 assLaw 𝑚 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cassintop	⊢ assIntOp
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vo	⊢ 𝑜
4		cclintop	⊢ clIntOp
5	1	cv	⊢ 𝑚
6	5 4	cfv	⊢ ( clIntOp ‘ 𝑚 )
7	3	cv	⊢ 𝑜
8		casslaw	⊢ assLaw
9	7 5 8	wbr	⊢ 𝑜 assLaw 𝑚
10	9 3 6	crab	⊢ { 𝑜 ∈ ( clIntOp ‘ 𝑚 ) ∣ 𝑜 assLaw 𝑚 }
11	1 2 10	cmpt	⊢ ( 𝑚 ∈ V ↦ { 𝑜 ∈ ( clIntOp ‘ 𝑚 ) ∣ 𝑜 assLaw 𝑚 } )
12	0 11	wceq	⊢ assIntOp = ( 𝑚 ∈ V ↦ { 𝑜 ∈ ( clIntOp ‘ 𝑚 ) ∣ 𝑜 assLaw 𝑚 } )