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=BaseM
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=BaseM
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∈BC≠c
10 6 7 8 9 syl3anc ⊢C∈B∧1<B→∃c∈BC≠c
11 df-ne ⊢C≠c↔¬C=c
12 11 rexbii ⊢∃c∈BC≠c↔∃c∈B¬C=c
13 rexnal ⊢∃c∈B¬C=c↔¬∀c∈BC=c
14 12 13 bitri ⊢∃c∈BC≠c↔¬∀c∈BC=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→ax∈B,y∈B⟼Cc=C
23 22 adantr ⊢φ∧a∈B∧c∈B∧ax∈B,y∈B⟼Cc=c→ax∈B,y∈B⟼Cc=C
24 simpr ⊢φ∧a∈B∧c∈B∧ax∈B,y∈B⟼Cc=c→ax∈B,y∈B⟼Cc=c
25 23 24 eqtr3d ⊢φ∧a∈B∧c∈B∧ax∈B,y∈B⟼Cc=c→C=c
26 25 ex ⊢φ∧a∈B∧c∈B→ax∈B,y∈B⟼Cc=c→C=c
27 26 ralimdva ⊢φ∧a∈B→∀c∈Bax∈B,y∈B⟼Cc=c→∀c∈BC=c
28 27 rexlimdva ⊢φ→∃a∈B∀c∈Bax∈B,y∈B⟼Cc=c→∀c∈BC=c
29 28 con3d ⊢φ→¬∀c∈BC=c→¬∃a∈B∀c∈Bax∈B,y∈B⟼Cc=c
30 rexnal ⊢∃c∈B¬ax∈B,y∈B⟼Cc=c↔¬∀c∈Bax∈B,y∈B⟼Cc=c
31 30 bicomi ⊢¬∀c∈Bax∈B,y∈B⟼Cc=c↔∃c∈B¬ax∈B,y∈B⟼Cc=c
32 31 ralbii ⊢∀a∈B¬∀c∈Bax∈B,y∈B⟼Cc=c↔∀a∈B∃c∈B¬ax∈B,y∈B⟼Cc=c
33 ralnex ⊢∀a∈B¬∀c∈Bax∈B,y∈B⟼Cc=c↔¬∃a∈B∀c∈Bax∈B,y∈B⟼Cc=c
34 df-ne ⊢ax∈B,y∈B⟼Cc≠c↔¬ax∈B,y∈B⟼Cc=c
35 34 bicomi ⊢¬ax∈B,y∈B⟼Cc=c↔ax∈B,y∈B⟼Cc≠c
36 35 rexbii ⊢∃c∈B¬ax∈B,y∈B⟼Cc=c↔∃c∈Bax∈B,y∈B⟼Cc≠c
37 36 ralbii ⊢∀a∈B∃c∈B¬ax∈B,y∈B⟼Cc=c↔∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c
38 32 33 37 3bitr3i ⊢¬∃a∈B∀c∈Bax∈B,y∈B⟼Cc=c↔∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c
39 29 38 imbitrdi ⊢φ→¬∀c∈BC=c→∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c
40 14 39 biimtrid ⊢φ→∃c∈BC≠c→∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c
41 10 40 syl5 ⊢φ→C∈B∧1<B→∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c
42 3 4 41 mp2and ⊢φ→∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c
43 2 eqcomi ⊢x∈B,y∈B⟼C=+M
44 1 43 isnmnd ⊢∀a∈B∃c∈Bax∈B,y∈B⟼Cc≠c→M∉Mnd
45 42 44 syl ⊢φ→M∉Mnd