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 ) )