Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-assintop Structured version   Visualization version   GIF version

Definition df-assintop 45373
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
StepHypRef Expression
1 cassintop 45370 . 2 class assIntOp
2 vm . . 3 setvar 𝑚
3 cvv 3429 . . 3 class V
4 vo . . . . . 6 setvar 𝑜
54cv 1538 . . . . 5 class 𝑜
62cv 1538 . . . . 5 class 𝑚
7 casslaw 45356 . . . . 5 class assLaw
85, 6, 7wbr 5073 . . . 4 wff 𝑜 assLaw 𝑚
9 cclintop 45369 . . . . 5 class clIntOp
106, 9cfv 6426 . . . 4 class ( clIntOp ‘𝑚)
118, 4, 10crab 3068 . . 3 class {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}
122, 3, 11cmpt 5156 . 2 class (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})
131, 12wceq 1539 1 wff assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})
Colors of variables: wff setvar class
This definition is referenced by:  assintopval  45377
  Copyright terms: Public domain W3C validator