Definition df-assintop 48117

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

Distinct variable group:   𝑚,𝑜

Detailed syntax breakdown of Definition df-assintop

Step	Hyp	Ref	Expression
1		cassintop 48114	. 2 class assIntOp
2		vm	. . 3 setvar 𝑚
3		cvv 3480	. . 3 class V
4		vo	. . . . . 6 setvar 𝑜
5	4	cv 1539	. . . . 5 class 𝑜
6	2	cv 1539	. . . . 5 class 𝑚
7		casslaw 48100	. . . . 5 class assLaw
8	5, 6, 7	wbr 5143	. . . 4 wff 𝑜 assLaw 𝑚
9		cclintop 48113	. . . . 5 class clIntOp
10	6, 9	cfv 6561	. . . 4 class ( clIntOp ‘𝑚)
11	8, 4, 10	crab 3436	. . 3 class {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}
12	2, 3, 11	cmpt 5225	. 2 class (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})
13	1, 12	wceq 1540	1 wff assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})

This definition is referenced by:  assintopval  48121