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=\left\{A,B\right\}$$
	mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
	mgm2nsgrp.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(\left(x=A\wedge y=A\right),B,A\right)\right)$$
Assertion	mgm2nsgrp	Could not format assertion : No typesetting found for |- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
2		mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
3		mgm2nsgrp.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(\left(x=A\wedge y=A\right),B,A\right)\right)$$
4	1	hashprdifel	$$⊢\left|S\right|=2\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$
5	1 2 3	mgm2nsgrplem1	$$⊢\left(A\in S\wedge B\in S\right)\to M\in \mathrm{Mgm}$$
6	5	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to M\in \mathrm{Mgm}$$
7	4 6	syl	$$⊢\left|S\right|=2\to M\in \mathrm{Mgm}$$
8	1 2 3	mgm2nsgrplem4	Could not format ( ( # ` S ) = 2 -> M e/ Smgrp ) : No typesetting found for |- ( ( # ` S ) = 2 -> M e/ Smgrp ) with typecode |-
9	7 8	jca	Could not format ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) ) : No typesetting found for |- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) ) with typecode |-