Metamath Proof Explorer

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 ⊢ Mnd = g ∈ Smgrp | [˙Base g / b]˙ [˙+ g / p]˙ ∃ e ∈ b ∀ x ∈ b e p x = x ∧ x p e = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmnd class Mnd
1 vg setvar g
2 csgrp class Smgrp
3 cbs class Base
4 1 cv setvar g
5 4 3 cfv class Base g
6 vb setvar b
7 cplusg class + 𝑔
8 4 7 cfv class + g
9 vp setvar p
10 ve setvar e
11 6 cv setvar b
12 vx setvar x
13 10 cv setvar e
14 9 cv setvar p
15 12 cv setvar x
16 13 15 14 co class e p x
17 16 15 wceq wff e p x = x
18 15 13 14 co class x p e
19 18 15 wceq wff x p e = x
20 17 19 wa wff e p x = x ∧ x p e = x
21 20 12 11 wral wff ∀ x ∈ b e p x = x ∧ x p e = x
22 21 10 11 wrex wff ∃ e ∈ b ∀ x ∈ b e p x = x ∧ x p e = x
23 22 9 8 wsbc wff [˙+ g / p]˙ ∃ e ∈ b ∀ x ∈ b e p x = x ∧ x p e = x
24 23 6 5 wsbc wff [˙Base g / b]˙ [˙+ g / p]˙ ∃ e ∈ b ∀ x ∈ b e p x = x ∧ x p e = x
25 24 1 2 crab class g ∈ Smgrp | [˙Base g / b]˙ [˙+ g / p]˙ ∃ e ∈ b ∀ x ∈ b e p x = x ∧ x p e = x
26 0 25 wceq wff Mnd = g ∈ Smgrp | [˙Base g / b]˙ [˙+ g / p]˙ ∃ e ∈ b ∀ x ∈ b e p x = x ∧ x p e = x