Metamath Proof Explorer

Theorem copisnmnd

Description: A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020)

Ref Expression
Hypotheses copisnmnd.b ⊢ B = Base M
copisnmnd.p ⊢ + M = x ∈ B , y ∈ B ⟼ C
copisnmnd.c ⊢ φ → C ∈ B
copisnmnd.n ⊢ φ → 1 < B
Assertion copisnmnd ⊢ φ → M ∉ Mnd

Proof

Step Hyp Ref Expression
1 copisnmnd.b ⊢ B = Base M
2 copisnmnd.p ⊢ + M = x ∈ B , y ∈ B ⟼ C
3 copisnmnd.c ⊢ φ → C ∈ B
4 copisnmnd.n ⊢ φ → 1 < B
5 1 fvexi ⊢ B ∈ V
6 5 a1i ⊢ C ∈ B ∧ 1 < B → B ∈ V
7 simpr ⊢ C ∈ B ∧ 1 < B → 1 < B
8 simpl ⊢ C ∈ B ∧ 1 < B → C ∈ B
9 hashgt12el2 ⊢ B ∈ V ∧ 1 < B ∧ C ∈ B → ∃ c ∈ B C ≠ c
10 6 7 8 9 syl3anc ⊢ C ∈ B ∧ 1 < B → ∃ c ∈ B C ≠ c
11 df-ne ⊢ C ≠ c ↔ ¬ C = c
12 11 rexbii ⊢ ∃ c ∈ B C ≠ c ↔ ∃ c ∈ B ¬ C = c
13 rexnal ⊢ ∃ c ∈ B ¬ C = c ↔ ¬ ∀ c ∈ B C = c
14 12 13 bitri ⊢ ∃ c ∈ B C ≠ c ↔ ¬ ∀ c ∈ B C = c
15 eqidd ⊢ φ ∧ a ∈ B ∧ c ∈ B → x ∈ B , y ∈ B ⟼ C = x ∈ B , y ∈ B ⟼ C
16 eqidd ⊢ φ ∧ a ∈ B ∧ c ∈ B ∧ x = a ∧ y = c → C = C
17 simpr ⊢ φ ∧ a ∈ B → a ∈ B
18 17 adantr ⊢ φ ∧ a ∈ B ∧ c ∈ B → a ∈ B
19 simpr ⊢ φ ∧ a ∈ B ∧ c ∈ B → c ∈ B
20 3 adantr ⊢ φ ∧ a ∈ B → C ∈ B
21 20 adantr ⊢ φ ∧ a ∈ B ∧ c ∈ B → C ∈ B
22 15 16 18 19 21 ovmpod ⊢ φ ∧ a ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C c = C
23 22 adantr ⊢ φ ∧ a ∈ B ∧ c ∈ B ∧ a x ∈ B , y ∈ B ⟼ C c = c → a x ∈ B , y ∈ B ⟼ C c = C
24 simpr ⊢ φ ∧ a ∈ B ∧ c ∈ B ∧ a x ∈ B , y ∈ B ⟼ C c = c → a x ∈ B , y ∈ B ⟼ C c = c
25 23 24 eqtr3d ⊢ φ ∧ a ∈ B ∧ c ∈ B ∧ a x ∈ B , y ∈ B ⟼ C c = c → C = c
26 25 ex ⊢ φ ∧ a ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C c = c → C = c
27 26 ralimdva ⊢ φ ∧ a ∈ B → ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c → ∀ c ∈ B C = c
28 27 rexlimdva ⊢ φ → ∃ a ∈ B ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c → ∀ c ∈ B C = c
29 28 con3d ⊢ φ → ¬ ∀ c ∈ B C = c → ¬ ∃ a ∈ B ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c
30 rexnal ⊢ ∃ c ∈ B ¬ a x ∈ B , y ∈ B ⟼ C c = c ↔ ¬ ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c
31 30 bicomi ⊢ ¬ ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c ↔ ∃ c ∈ B ¬ a x ∈ B , y ∈ B ⟼ C c = c
32 31 ralbii ⊢ ∀ a ∈ B ¬ ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c ↔ ∀ a ∈ B ∃ c ∈ B ¬ a x ∈ B , y ∈ B ⟼ C c = c
33 ralnex ⊢ ∀ a ∈ B ¬ ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c ↔ ¬ ∃ a ∈ B ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c
34 df-ne ⊢ a x ∈ B , y ∈ B ⟼ C c ≠ c ↔ ¬ a x ∈ B , y ∈ B ⟼ C c = c
35 34 bicomi ⊢ ¬ a x ∈ B , y ∈ B ⟼ C c = c ↔ a x ∈ B , y ∈ B ⟼ C c ≠ c
36 35 rexbii ⊢ ∃ c ∈ B ¬ a x ∈ B , y ∈ B ⟼ C c = c ↔ ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
37 36 ralbii ⊢ ∀ a ∈ B ∃ c ∈ B ¬ a x ∈ B , y ∈ B ⟼ C c = c ↔ ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
38 32 33 37 3bitr3i ⊢ ¬ ∃ a ∈ B ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C c = c ↔ ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
39 29 38 imbitrdi ⊢ φ → ¬ ∀ c ∈ B C = c → ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
40 14 39 biimtrid ⊢ φ → ∃ c ∈ B C ≠ c → ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
41 10 40 syl5 ⊢ φ → C ∈ B ∧ 1 < B → ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
42 3 4 41 mp2and ⊢ φ → ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c
43 2 eqcomi ⊢ x ∈ B , y ∈ B ⟼ C = + M
44 1 43 isnmnd ⊢ ∀ a ∈ B ∃ c ∈ B a x ∈ B , y ∈ B ⟼ C c ≠ c → M ∉ Mnd
45 42 44 syl ⊢ φ → M ∉ Mnd