Theorem mgm2nsgrp

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

	Ref	Expression
Hypotheses	mgm2nsgrp.s	|- S = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
Assertion	mgm2nsgrp	|- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
4	1	hashprdifel	|- ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )
5	1 2 3	mgm2nsgrplem1	|- ( ( A e. S /\ B e. S ) -> M e. Mgm )
6	5	3adant3	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> M e. Mgm )
7	4 6	syl	|- ( ( # ` S ) = 2 -> M e. Mgm )
8	1 2 3	mgm2nsgrplem4	|- ( ( # ` S ) = 2 -> M e/ Smgrp )
9	7 8	jca	|- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) )