Definition df-mnd 18395

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

Assertion

Ref	Expression
df-mnd	⊢ Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}

Distinct variable group:   𝑒,𝑏,𝑔,𝑝,𝑥

Detailed syntax breakdown of Definition df-mnd

Step	Hyp	Ref	Expression
1		cmnd 18394	. 2 class Mnd
2		ve	. . . . . . . . . . 11 setvar 𝑒
3	2	cv 1538	. . . . . . . . . 10 class 𝑒
4		vx	. . . . . . . . . . 11 setvar 𝑥
5	4	cv 1538	. . . . . . . . . 10 class 𝑥
6		vp	. . . . . . . . . . 11 setvar 𝑝
7	6	cv 1538	. . . . . . . . . 10 class 𝑝
8	3, 5, 7	co 7284	. . . . . . . . 9 class (𝑒𝑝𝑥)
9	8, 5	wceq 1539	. . . . . . . 8 wff (𝑒𝑝𝑥) = 𝑥
10	5, 3, 7	co 7284	. . . . . . . . 9 class (𝑥𝑝𝑒)
11	10, 5	wceq 1539	. . . . . . . 8 wff (𝑥𝑝𝑒) = 𝑥
12	9, 11	wa 396	. . . . . . 7 wff ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
13		vb	. . . . . . . 8 setvar 𝑏
14	13	cv 1538	. . . . . . 7 class 𝑏
15	12, 4, 14	wral 3065	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
16	15, 2, 14	wrex 3066	. . . . 5 wff ∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
17		vg	. . . . . . 7 setvar 𝑔
18	17	cv 1538	. . . . . 6 class 𝑔
19		cplusg 16971	. . . . . 6 class +g
20	18, 19	cfv 6437	. . . . 5 class (+g‘𝑔)
21	16, 6, 20	wsbc 3717	. . . 4 wff [(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
22		cbs 16921	. . . . 5 class Base
23	18, 22	cfv 6437	. . . 4 class (Base‘𝑔)
24	21, 13, 23	wsbc 3717	. . 3 wff [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
25		csgrp 18383	. . 3 class Smgrp
26	24, 17, 25	crab 3069	. 2 class {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
27	1, 26	wceq 1539	1 wff Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}

This definition is referenced by:  ismnddef  18396  bj-mndsssmgrp  35450