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

Definition df-clintop 41624
Description: Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of [Hall] p. 2, definition in section I.1 of [Bruck] p. 1, or definition 1 in [BourbakiAlg1] p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020.)
Assertion
Ref Expression
df-clintop clIntOp = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))

Detailed syntax breakdown of Definition df-clintop
StepHypRef Expression
1 cclintop 41621 . 2 class clIntOp
2 vm . . 3 setvar 𝑚
3 cvv 3168 . . 3 class V
42cv 1473 . . . 4 class 𝑚
5 cintop 41620 . . . 4 class intOp
64, 4, 5co 6523 . . 3 class (𝑚 intOp 𝑚)
72, 3, 6cmpt 4633 . 2 class (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))
81, 7wceq 1474 1 wff clIntOp = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))
Colors of variables: wff setvar class
This definition is referenced by:  clintopval  41628
  Copyright terms: Public domain W3C validator