Theorem sgrp2nmnd

Description: A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020)

	Ref	Expression
Hypotheses	mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
	mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
	sgrp2nmnd.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(x=A,A,B\right)\right)$$
Assertion	sgrp2nmnd	$$⊢\left|S\right|=2\to \left(M\in \mathrm{Smgrp}\wedge M\notin \mathrm{Mnd}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
2		mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
3		sgrp2nmnd.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(x=A,A,B\right)\right)$$
4	1 2 3	sgrp2nmndlem4	$$⊢\left|S\right|=2\to M\in \mathrm{Smgrp}$$
5	1 2 3	sgrp2nmndlem5	$$⊢\left|S\right|=2\to M\notin \mathrm{Mnd}$$
6	4 5	jca	$$⊢\left|S\right|=2\to \left(M\in \mathrm{Smgrp}\wedge M\notin \mathrm{Mnd}\right)$$