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	Could not format assertion : No typesetting found for |- ( ( # ` S ) = 2 -> ( M e. Smgrp /\ M e/ Mnd ) ) with typecode |-

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	Could not format ( ( # ` S ) = 2 -> M e. Smgrp ) : No typesetting found for |- ( ( # ` S ) = 2 -> M e. Smgrp ) with typecode |-
5	1 2 3	sgrp2nmndlem5	$$⊢\left|S\right|=2\to M\notin \mathrm{Mnd}$$
6	4 5	jca	Could not format ( ( # ` S ) = 2 -> ( M e. Smgrp /\ M e/ Mnd ) ) : No typesetting found for |- ( ( # ` S ) = 2 -> ( M e. Smgrp /\ M e/ Mnd ) ) with typecode |-