Definition df-mnd 13450

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 13456), whose operation is associative (see mndass 13457) and has a two-sided neutral element (see mndid 13458), see also ismnd 13452. (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

Step	Hyp	Ref	Expression
1		cmnd 13449	. 2 class Mnd
2		ve	. . . . . . . . . . 11 setvar e
3	2	cv 1394	. . . . . . . . . 10 class e
4		vx	. . . . . . . . . . 11 setvar x
5	4	cv 1394	. . . . . . . . . 10 class x
6		vp	. . . . . . . . . . 11 setvar p
7	6	cv 1394	. . . . . . . . . 10 class p
8	3, 5, 7	co 6001	. . . . . . . . 9 class ( e p x )
9	8, 5	wceq 1395	. . . . . . . 8 wff ( e p x ) = x
10	5, 3, 7	co 6001	. . . . . . . . 9 class ( x p e )
11	10, 5	wceq 1395	. . . . . . . 8 wff ( x p e ) = x
12	9, 11	wa 104	. . . . . . 7 wff ( ( e p x ) = x /\ ( x p e ) = x )
13		vb	. . . . . . . 8 setvar b
14	13	cv 1394	. . . . . . 7 class b
15	12, 4, 14	wral 2508	. . . . . 6 wff A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
16	15, 2, 14	wrex 2509	. . . . 5 wff E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
17		vg	. . . . . . 7 setvar g
18	17	cv 1394	. . . . . 6 class g
19		cplusg 13110	. . . . . 6 class +g
20	18, 19	cfv 5318	. . . . 5 class ( +g ` g )
21	16, 6, 20	wsbc 3028	. . . 4 wff [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
22		cbs 13032	. . . . 5 class Base
23	18, 22	cfv 5318	. . . 4 class ( Base ` g )
24	21, 13, 23	wsbc 3028	. . 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 13434	. . 3 class Smgrp
26	24, 17, 25	crab 2512	. 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 ) }
27	1, 26	wceq 1395	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 ) }

This definition is referenced by:  ismnddef  13451