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