Theorem mndsgrp

Description: A monoid is a semigroup. (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020) (Proof shortened by AV, 6-Feb-2020)

	Ref	Expression
Assertion	mndsgrp	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2		eqid	$$⊢{+}_G={+}_G$$
3	1 2	ismnddef	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(G\in \mathrm{Smgrp}\wedge \exists e\in {\mathrm{Base}}_G\forall x\in {\mathrm{Base}}_G\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
4	3	simplbi	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Smgrp}$$