Users' Mathboxes 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 41628
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 41624 . 2 class SGrpALT
2 vg . . . . . 6 setvar 𝑔
32cv 1473 . . . . 5 class 𝑔
4 cplusg 15716 . . . . 5 class +g
53, 4cfv 5789 . . . 4 class (+g𝑔)
6 cbs 15643 . . . . 5 class Base
73, 6cfv 5789 . . . 4 class (Base‘𝑔)
8 casslaw 41591 . . . 4 class assLaw
95, 7, 8wbr 4577 . . 3 wff (+g𝑔) assLaw (Base‘𝑔)
10 cmgm2 41622 . . 3 class MgmALT
119, 2, 10crab 2899 . 2 class {𝑔 ∈ MgmALT ∣ (+g𝑔) assLaw (Base‘𝑔)}
121, 11wceq 1474 1 wff SGrpALT = {𝑔 ∈ MgmALT ∣ (+g𝑔) assLaw (Base‘𝑔)}
Colors of variables: wff setvar class
This definition is referenced by:  issgrpALT  41632
  Copyright terms: Public domain W3C validator