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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
copisnmnd.p ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
copisnmnd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
copisnmnd.n ⊢ ( 𝜑 → 1 < ( ♯ ‘ 𝐵 ) )
Assertion copisnmnd ( 𝜑 → 𝑀 ∉ Mnd )

Proof

Step Hyp Ref Expression
1 copisnmnd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 copisnmnd.p ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3 copisnmnd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
4 copisnmnd.n ⊢ ( 𝜑 → 1 < ( ♯ ‘ 𝐵 ) )
5 1 fvexi ⊢ 𝐵 ∈ V
6 5 a1i ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 𝐵 ∈ V )
7 simpr ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 1 < ( ♯ ‘ 𝐵 ) )
8 simpl ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
9 hashgt12el2 ⊢ ( ( 𝐵 ∈ V ∧ 1 < ( ♯ ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑐 ∈ 𝐵 𝐶 ≠ 𝑐 )
10 6 7 8 9 syl3anc ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑐 ∈ 𝐵 𝐶 ≠ 𝑐 )
11 df-ne ⊢ ( 𝐶 ≠ 𝑐 ↔ ¬ 𝐶 = 𝑐 )
12 11 rexbii ⊢ ( ∃ 𝑐 ∈ 𝐵 𝐶 ≠ 𝑐 ↔ ∃ 𝑐 ∈ 𝐵 ¬ 𝐶 = 𝑐 )
13 rexnal ⊢ ( ∃ 𝑐 ∈ 𝐵 ¬ 𝐶 = 𝑐 ↔ ¬ ∀ 𝑐 ∈ 𝐵 𝐶 = 𝑐 )
14 12 13 bitri ⊢ ( ∃ 𝑐 ∈ 𝐵 𝐶 ≠ 𝑐 ↔ ¬ ∀ 𝑐 ∈ 𝐵 𝐶 = 𝑐 )
15 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
16 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑐 ) ) → 𝐶 = 𝐶 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ 𝐵 )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
22 15 16 18 19 21 ovmpod ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
23 22 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
24 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 )
25 23 24 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ) → 𝐶 = 𝑐 )
26 25 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 → 𝐶 = 𝑐 ) )
27 26 ralimdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 → ∀ 𝑐 ∈ 𝐵 𝐶 = 𝑐 ) )
28 27 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 → ∀ 𝑐 ∈ 𝐵 𝐶 = 𝑐 ) )
29 28 con3d ⊢ ( 𝜑 → ( ¬ ∀ 𝑐 ∈ 𝐵 𝐶 = 𝑐 → ¬ ∃ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ) )
30 rexnal ⊢ ( ∃ 𝑐 ∈ 𝐵 ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ¬ ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 )
31 30 bicomi ⊢ ( ¬ ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ∃ 𝑐 ∈ 𝐵 ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 )
32 31 ralbii ⊢ ( ∀ 𝑎 ∈ 𝐵 ¬ ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 )
33 ralnex ⊢ ( ∀ 𝑎 ∈ 𝐵 ¬ ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ¬ ∃ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 )
34 df-ne ⊢ ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 ↔ ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 )
35 34 bicomi ⊢ ( ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 )
36 35 rexbii ⊢ ( ∃ 𝑐 ∈ 𝐵 ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 )
37 36 ralbii ⊢ ( ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ¬ ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 )
38 32 33 37 3bitr3i ⊢ ( ¬ ∃ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝑐 ↔ ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 )
39 29 38 syl6ib ⊢ ( 𝜑 → ( ¬ ∀ 𝑐 ∈ 𝐵 𝐶 = 𝑐 → ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 ) )
40 14 39 syl5bi ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐵 𝐶 ≠ 𝑐 → ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 ) )
41 10 40 syl5 ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐵 ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 ) )
42 3 4 41 mp2and ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 )
43 2 eqcomi ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( +g ‘ 𝑀 )
44 1 43 isnmnd ⊢ ( ∀ 𝑎 ∈ 𝐵 ∃ 𝑐 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ≠ 𝑐 → 𝑀 ∉ Mnd )
45 42 44 syl ⊢ ( 𝜑 → 𝑀 ∉ Mnd )