Definition df-mnd

Description: Amonoid 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 ), whose operation is associative (see mndass ) and has a two-sided neutral element (see mndid ), see also ismnd . (Contributed by Mario Carneiro, 6-Jan-2015) (Revised by AV, 1-Feb-2020)

	Ref	Expression
Assertion	df-mnd	Could not format assertion : No typesetting found for |- 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 ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnd	$$class\mathrm{Mnd}$$
1		vg	$$setvarg$$
2		csgrp	Could not format Smgrp : No typesetting found for class Smgrp with typecode class
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class{\mathrm{Base}}_g$$
6		vb	$$setvarb$$
7		cplusg	$$class{+}_{𝑔}$$
8	4 7	cfv	$$class{+}_g$$
9		vp	$$setvarp$$
10		ve	$$setvare$$
11	6	cv	$$setvarb$$
12		vx	$$setvarx$$
13	10	cv	$$setvare$$
14	9	cv	$$setvarp$$
15	12	cv	$$setvarx$$
16	13 15 14	co	$$class\left(epx\right)$$
17	16 15	wceq	$$wffepx=x$$
18	15 13 14	co	$$class\left(xpe\right)$$
19	18 15	wceq	$$wffxpe=x$$
20	17 19	wa	$$wff\left(epx=x\wedge xpe=x\right)$$
21	20 12 11	wral	$$wff\forall x\in b\left(epx=x\wedge xpe=x\right)$$
22	21 10 11	wrex	$$wff\exists e\in b\forall x\in b\left(epx=x\wedge xpe=x\right)$$
23	22 9 8	wsbc	$$wff\underset{\dot{}}{[}{+}_g/p\underset{\dot{}}{]}\exists e\in b\forall x\in b\left(epx=x\wedge xpe=x\right)$$
24	23 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/p\underset{\dot{}}{]}\exists e\in b\forall x\in b\left(epx=x\wedge xpe=x\right)$$
25	24 1 2	crab	Could not format { 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 ) } : No typesetting found for 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 ) } with typecode class
26	0 25	wceq	Could not format 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 ) } : No typesetting found for 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 ) } with typecode wff