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

Definition df-sgrp2 41647
 Description: A semigroup is a magma with an associative operation. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4, or of a semi-group in section 1.3 of [Hall] p. 7. (Contributed by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-sgrp2 SGrpALT = {𝑔 ∈ MgmALT ∣ (+g𝑔) assLaw (Base‘𝑔)}

Detailed syntax breakdown of Definition df-sgrp2
StepHypRef Expression
1 csgrp2 41643 . 2 class SGrpALT
2 vg . . . . . 6 setvar 𝑔
32cv 1474 . . . . 5 class 𝑔
4 cplusg 15768 . . . . 5 class +g
53, 4cfv 5804 . . . 4 class (+g𝑔)
6 cbs 15695 . . . . 5 class Base
73, 6cfv 5804 . . . 4 class (Base‘𝑔)
8 casslaw 41610 . . . 4 class assLaw
95, 7, 8wbr 4583 . . 3 wff (+g𝑔) assLaw (Base‘𝑔)
10 cmgm2 41641 . . 3 class MgmALT
119, 2, 10crab 2900 . 2 class {𝑔 ∈ MgmALT ∣ (+g𝑔) assLaw (Base‘𝑔)}
121, 11wceq 1475 1 wff SGrpALT = {𝑔 ∈ MgmALT ∣ (+g𝑔) assLaw (Base‘𝑔)}
 Colors of variables: wff setvar class This definition is referenced by:  issgrpALT  41651
 Copyright terms: Public domain W3C validator