Metamath Proof Explorer

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 ∈ V ⟼ o ∈ clIntOp ⁡ m | o assLaw m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cassintop class assIntOp
1 vm setvar m
2 cvv class V
3 vo setvar o
4 cclintop class clIntOp
5 1 cv setvar m
6 5 4 cfv class clIntOp ⁡ m
7 3 cv setvar o
8 casslaw class assLaw
9 7 5 8 wbr wff o assLaw m
10 9 3 6 crab class o ∈ clIntOp ⁡ m | o assLaw m
11 1 2 10 cmpt class m ∈ V ⟼ o ∈ clIntOp ⁡ m | o assLaw m
12 0 11 wceq wff assIntOp = m ∈ V ⟼ o ∈ clIntOp ⁡ m | o assLaw m