Metamath Proof Explorer

Theorem mgmnsgrpex

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

Ref Expression
Assertion mgmnsgrpex ⊢ ∃ m ∈ Mgm m ∉ Smgrp

Proof

Step Hyp Ref Expression
1 prhash2ex ⊢ 0 1 = 2
2 c0ex ⊢ 0 ∈ V
3 1ex ⊢ 1 ∈ V
4 2 3 pm3.2i ⊢ 0 ∈ V ∧ 1 ∈ V
5 eqid ⊢ 0 1 = 0 1
6 prex ⊢ 0 1 ∈ V
7 eqeq1 ⊢ x = u → x = 0 ↔ u = 0
8 7 anbi1d ⊢ x = u → x = 0 ∧ y = 0 ↔ u = 0 ∧ y = 0
9 8 ifbid ⊢ x = u → if x = 0 ∧ y = 0 1 0 = if u = 0 ∧ y = 0 1 0
10 eqeq1 ⊢ y = v → y = 0 ↔ v = 0
11 10 anbi2d ⊢ y = v → u = 0 ∧ y = 0 ↔ u = 0 ∧ v = 0
12 11 ifbid ⊢ y = v → if u = 0 ∧ y = 0 1 0 = if u = 0 ∧ v = 0 1 0
13 9 12 cbvmpov ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 = u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0
14 13 opeq2i ⊢ + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 = + ndx u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0
15 14 preq2i ⊢ Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 = Base ndx 0 1 + ndx u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0
16 15 grpbase ⊢ 0 1 ∈ V → 0 1 = Base Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0
17 6 16 ax-mp ⊢ 0 1 = Base Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0
18 17 eqcomi ⊢ Base Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 = 0 1
19 6 6 mpoex ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0 ∈ V
20 15 grpplusg ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0 ∈ V → u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0 = + Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0
21 19 20 ax-mp ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0 = + Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0
22 21 eqcomi ⊢ + Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 = u ∈ 0 1 , v ∈ 0 1 ⟼ if u = 0 ∧ v = 0 1 0
23 5 18 22 mgm2nsgrplem1 ⊢ 0 ∈ V ∧ 1 ∈ V → Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 ∈ Mgm
24 4 23 mp1i ⊢ 0 1 = 2 → Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 ∈ Mgm
25 neleq1 ⊢ m = Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 → m ∉ Smgrp ↔ Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 ∉ Smgrp
26 25 adantl ⊢ 0 1 = 2 ∧ m = Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 → m ∉ Smgrp ↔ Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 ∉ Smgrp
27 5 18 22 mgm2nsgrplem4 ⊢ 0 1 = 2 → Base ndx 0 1 + ndx x ∈ 0 1 , y ∈ 0 1 ⟼ if x = 0 ∧ y = 0 1 0 ∉ Smgrp
28 24 26 27 rspcedvd ⊢ 0 1 = 2 → ∃ m ∈ Mgm m ∉ Smgrp
29 1 28 ax-mp ⊢ ∃ m ∈ Mgm m ∉ Smgrp