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 41627
 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 41624 . 2 class assIntOp
2 vm . . 3 setvar 𝑚
3 cvv 3173 . . 3 class V
4 vo . . . . . 6 setvar 𝑜
54cv 1474 . . . . 5 class 𝑜
62cv 1474 . . . . 5 class 𝑚
7 casslaw 41610 . . . . 5 class assLaw
85, 6, 7wbr 4583 . . . 4 wff 𝑜 assLaw 𝑚
9 cclintop 41623 . . . . 5 class clIntOp
106, 9cfv 5804 . . . 4 class ( clIntOp ‘𝑚)
118, 4, 10crab 2900 . . 3 class {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}
122, 3, 11cmpt 4643 . 2 class (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})
131, 12wceq 1475 1 wff assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})
 Colors of variables: wff setvar class This definition is referenced by:  assintopval  41631
 Copyright terms: Public domain W3C validator