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 42635
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 42632 . 2 class clIntOp
2 vm . . 3 setvar 𝑚
3 cvv 3385 . . 3 class V
42cv 1652 . . . 4 class 𝑚
5 cintop 42631 . . . 4 class intOp
64, 4, 5co 6878 . . 3 class (𝑚 intOp 𝑚)
72, 3, 6cmpt 4922 . 2 class (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))
81, 7wceq 1653 1 wff clIntOp = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))
Colors of variables: wff setvar class
This definition is referenced by:  clintopval  42639
  Copyright terms: Public domain W3C validator