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

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
2		mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
3		sgrp2nmnd.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
4	1 2 3	sgrp2nmndlem4	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∈ Smgrp )
5	1 2 3	sgrp2nmndlem5	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∉ Mnd )
6	4 5	jca	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝑀 ∈ Smgrp ∧ 𝑀 ∉ Mnd ) )