ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mnd Unicode version

Definition df-mnd 12707
Description: A monoid is a semigroup, which has a two-sided neutral element. Definition 2 in [BourbakiAlg1] p. 12. In other words (according to the definition in [Lang] p. 3), a monoid is a set equipped with an everywhere defined internal operation (see mndcl 12713), whose operation is associative (see mndass 12714) and has a two-sided neutral element (see mndid 12715), see also ismnd 12709. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
Assertion
Ref Expression
df-mnd  |-  Mnd  =  { g  e. Smgrp  |  [. ( Base `  g
)  /  b ]. [. ( +g  `  g
)  /  p ]. E. e  e.  b  A. x  e.  b 
( ( e p x )  =  x  /\  ( x p e )  =  x ) }
Distinct variable group:    e, b, g, p, x

Detailed syntax breakdown of Definition df-mnd
StepHypRef Expression
1 cmnd 12706 . 2  class  Mnd
2 ve . . . . . . . . . . 11  setvar  e
32cv 1352 . . . . . . . . . 10  class  e
4 vx . . . . . . . . . . 11  setvar  x
54cv 1352 . . . . . . . . . 10  class  x
6 vp . . . . . . . . . . 11  setvar  p
76cv 1352 . . . . . . . . . 10  class  p
83, 5, 7co 5869 . . . . . . . . 9  class  ( e p x )
98, 5wceq 1353 . . . . . . . 8  wff  ( e p x )  =  x
105, 3, 7co 5869 . . . . . . . . 9  class  ( x p e )
1110, 5wceq 1353 . . . . . . . 8  wff  ( x p e )  =  x
129, 11wa 104 . . . . . . 7  wff  ( ( e p x )  =  x  /\  (
x p e )  =  x )
13 vb . . . . . . . 8  setvar  b
1413cv 1352 . . . . . . 7  class  b
1512, 4, 14wral 2455 . . . . . 6  wff  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
1615, 2, 14wrex 2456 . . . . 5  wff  E. e  e.  b  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
17 vg . . . . . . 7  setvar  g
1817cv 1352 . . . . . 6  class  g
19 cplusg 12515 . . . . . 6  class  +g
2018, 19cfv 5212 . . . . 5  class  ( +g  `  g )
2116, 6, 20wsbc 2962 . . . 4  wff  [. ( +g  `  g )  /  p ]. E. e  e.  b  A. x  e.  b  ( ( e p x )  =  x  /\  ( x p e )  =  x )
22 cbs 12442 . . . . 5  class  Base
2318, 22cfv 5212 . . . 4  class  ( Base `  g )
2421, 13, 23wsbc 2962 . . 3  wff  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  p ]. E. e  e.  b 
A. x  e.  b  ( ( e p x )  =  x  /\  ( x p e )  =  x )
25 csgrp 12696 . . 3  class Smgrp
2624, 17, 25crab 2459 . 2  class  { g  e. Smgrp  |  [. ( Base `  g )  /  b ]. [. ( +g  `  g
)  /  p ]. E. e  e.  b  A. x  e.  b 
( ( e p x )  =  x  /\  ( x p e )  =  x ) }
271, 26wceq 1353 1  wff  Mnd  =  { g  e. Smgrp  |  [. ( Base `  g
)  /  b ]. [. ( +g  `  g
)  /  p ]. E. e  e.  b  A. x  e.  b 
( ( e p x )  =  x  /\  ( x p e )  =  x ) }
Colors of variables: wff set class
This definition is referenced by:  ismnddef  12708
  Copyright terms: Public domain W3C validator