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 = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
Assertion	sgrp2nmnd	|- ( ( # ` S ) = 2 -> ( M e. Smgrp /\ M e/ Mnd ) )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
4	1 2 3	sgrp2nmndlem4	|- ( ( # ` S ) = 2 -> M e. Smgrp )
5	1 2 3	sgrp2nmndlem5	|- ( ( # ` S ) = 2 -> M e/ Mnd )
6	4 5	jca	|- ( ( # ` S ) = 2 -> ( M e. Smgrp /\ M e/ Mnd ) )