Metamath Proof Explorer

Theorem sgrpnmndex

Description: There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020)

Ref Expression
Assertion sgrpnmndex ⊢ ∃ m ∈ Smgrp m ∉ Mnd

Proof

Step Hyp Ref Expression
1 prhash2ex ⊢ 0 1 = 2
2 eqid ⊢ 0 1 = 0 1
3 prex ⊢ 0 1 ∈ V
4 eqeq1 ⊢ x = u → x = 0 ↔ u = 0
5 4 ifbid ⊢ x = u → if x = 0 0 1 = if u = 0 0 1
6 eqidd ⊢ y = v → if u = 0 0 1 = if u = 0 0 1
7 5 6 cbvmpov ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 = u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1
8 7 opeq2i ⊢ + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 = + ndx u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1
9 8 preq2i ⊢ Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 = Base ndx 0 1 + ndx u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1
10 9 grpbase ⊢ 0 1 ∈ V → 0 1 = Base Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1
11 3 10 ax-mp ⊢ 0 1 = Base Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1
12 11 eqcomi ⊢ Base Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 = 0 1
13 3 3 mpoex ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1 ∈ V
14 9 grpplusg ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1 ∈ V → u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1 = + Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1
15 13 14 ax-mp ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1 = + Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1
16 15 eqcomi ⊢ + Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 = u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 0 1
17 2 12 16 sgrp2nmndlem4 ⊢ 0 1 = 2 → Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 ∈ Smgrp
18 neleq1 ⊢ m = Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 → m ∉ Mnd ↔ Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 ∉ Mnd
19 18 adantl ⊢ 0 1 = 2 ∧ m = Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 → m ∉ Mnd ↔ Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 ∉ Mnd
20 2 12 16 sgrp2nmndlem5 ⊢ 0 1 = 2 → Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 0 1 ∉ Mnd
21 17 19 20 rspcedvd ⊢ 0 1 = 2 → ∃ m ∈ Smgrp m ∉ Mnd
22 1 21 ax-mp ⊢ ∃ m ∈ Smgrp m ∉ Mnd