Metamath Proof Explorer


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 𝑆 = { 𝐴 , 𝐵 }
mgm2nsgrp.b ( Base ‘ 𝑀 ) = 𝑆
mgm2nsgrp.o ( +g𝑀 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
Assertion mgm2nsgrp ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝑀 ∈ Mgm ∧ 𝑀 ∉ Smgrp ) )

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s 𝑆 = { 𝐴 , 𝐵 }
2 mgm2nsgrp.b ( Base ‘ 𝑀 ) = 𝑆
3 mgm2nsgrp.o ( +g𝑀 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
4 1 hashprdifel ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) )
5 1 2 3 mgm2nsgrplem1 ( ( 𝐴𝑆𝐵𝑆 ) → 𝑀 ∈ Mgm )
6 5 3adant3 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → 𝑀 ∈ Mgm )
7 4 6 syl ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∈ Mgm )
8 1 2 3 mgm2nsgrplem4 ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∉ Smgrp )
9 7 8 jca ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝑀 ∈ Mgm ∧ 𝑀 ∉ Smgrp ) )