Metamath Proof Explorer

Theorem tworepnotupword

Description: Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024)

Ref Expression
Hypothesis tworepnotupword.1 ⊢ A ∈ V
Assertion tworepnotupword ⊢ ¬ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ∈ UpWord S

Proof

Step Hyp Ref Expression
1 tworepnotupword.1 ⊢ A ∈ V
2 ovex ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ∈ V
3 c0ex ⊢ 0 ∈ V
4 3 isseti ⊢ ∃ k k = 0
5 0z ⊢ 0 ∈ ℤ
6 ccat2s1len ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ = 2
7 6 oveq1i ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1 = 2 − 1
8 2m1e1 ⊢ 2 − 1 = 1
9 7 8 eqtri ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1 = 1
10 1z ⊢ 1 ∈ ℤ
11 9 10 eqeltri ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1 ∈ ℤ
12 0lt1 ⊢ 0 < 1
13 12 9 breqtrri ⊢ 0 < ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
14 fzolb ⊢ 0 ∈ 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1 ↔ 0 ∈ ℤ ∧ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1 ∈ ℤ ∧ 0 < ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
15 5 11 13 14 mpbir3an ⊢ 0 ∈ 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
16 eleq1a ⊢ 0 ∈ 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1 → k = 0 → k ∈ 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
17 15 16 ax-mp ⊢ k = 0 → k ∈ 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
18 fveq2 ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩
19 18 oveq1d ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b − 1 = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
20 19 oveq2d ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → 0 ..^ b − 1 = 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
21 20 eleq2d ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → k ∈ 0 ..^ b − 1 ↔ k ∈ 0 ..^ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ − 1
22 17 21 imbitrrid ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → k = 0 → k ∈ 0 ..^ b − 1
23 et-ltneverrefl ⊢ ¬ A < A
24 fveq1 ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b ⁡ 0 = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 0
25 ccat2s1p1 ⊢ A ∈ V → ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 0 = A
26 1 25 ax-mp ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 0 = A
27 24 26 eqtrdi ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b ⁡ 0 = A
28 fveq1 ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b ⁡ 0 + 1 = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 0 + 1
29 1e0p1 ⊢ 1 = 0 + 1
30 29 fveq2i ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 1 = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 0 + 1
31 ccat2s1p2 ⊢ A ∈ V → ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 1 = A
32 1 31 ax-mp ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 1 = A
33 30 32 eqtr3i ⊢ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ⁡ 0 + 1 = A
34 28 33 eqtrdi ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b ⁡ 0 + 1 = A
35 27 34 breq12d ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b ⁡ 0 < b ⁡ 0 + 1 ↔ A < A
36 23 35 mtbiri ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ¬ b ⁡ 0 < b ⁡ 0 + 1
37 fveq2 ⊢ k = 0 → b ⁡ k = b ⁡ 0
38 fvoveq1 ⊢ k = 0 → b ⁡ k + 1 = b ⁡ 0 + 1
39 37 38 breq12d ⊢ k = 0 → b ⁡ k < b ⁡ k + 1 ↔ b ⁡ 0 < b ⁡ 0 + 1
40 39 biimpd ⊢ k = 0 → b ⁡ k < b ⁡ k + 1 → b ⁡ 0 < b ⁡ 0 + 1
41 40 con3d ⊢ k = 0 → ¬ b ⁡ 0 < b ⁡ 0 + 1 → ¬ b ⁡ k < b ⁡ k + 1
42 36 41 syl5com ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → k = 0 → ¬ b ⁡ k < b ⁡ k + 1
43 22 42 jcad ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → k = 0 → k ∈ 0 ..^ b − 1 ∧ ¬ b ⁡ k < b ⁡ k + 1
44 43 eximdv ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ∃ k k = 0 → ∃ k k ∈ 0 ..^ b − 1 ∧ ¬ b ⁡ k < b ⁡ k + 1
45 4 44 mpi ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ∃ k k ∈ 0 ..^ b − 1 ∧ ¬ b ⁡ k < b ⁡ k + 1
46 nfre1 ⊢ Ⅎ k ∃ k ∈ 0 ..^ b − 1 ¬ b ⁡ k < b ⁡ k + 1
47 rspe ⊢ k ∈ 0 ..^ b − 1 ∧ ¬ b ⁡ k < b ⁡ k + 1 → ∃ k ∈ 0 ..^ b − 1 ¬ b ⁡ k < b ⁡ k + 1
48 46 47 exlimi ⊢ ∃ k k ∈ 0 ..^ b − 1 ∧ ¬ b ⁡ k < b ⁡ k + 1 → ∃ k ∈ 0 ..^ b − 1 ¬ b ⁡ k < b ⁡ k + 1
49 45 48 syl ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ∃ k ∈ 0 ..^ b − 1 ¬ b ⁡ k < b ⁡ k + 1
50 rexnal ⊢ ∃ k ∈ 0 ..^ b − 1 ¬ b ⁡ k < b ⁡ k + 1 ↔ ¬ ∀ k ∈ 0 ..^ b − 1 b ⁡ k < b ⁡ k + 1
51 49 50 sylib ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ¬ ∀ k ∈ 0 ..^ b − 1 b ⁡ k < b ⁡ k + 1
52 df-upword ⊢ UpWord S = b | b ∈ Word S ∧ ∀ k ∈ 0 ..^ b − 1 b ⁡ k < b ⁡ k + 1
53 52 eqabri ⊢ b ∈ UpWord S ↔ b ∈ Word S ∧ ∀ k ∈ 0 ..^ b − 1 b ⁡ k < b ⁡ k + 1
54 53 simprbi ⊢ b ∈ UpWord S → ∀ k ∈ 0 ..^ b − 1 b ⁡ k < b ⁡ k + 1
55 51 54 nsyl ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ¬ b ∈ UpWord S
56 eleq1 ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → b ∈ UpWord S ↔ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ∈ UpWord S
57 55 56 mtbid ⊢ b = ⟨“ A ”⟩ ++ ⟨“ A ”⟩ → ¬ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ∈ UpWord S
58 2 57 vtocle ⊢ ¬ ⟨“ A ”⟩ ++ ⟨“ A ”⟩ ∈ UpWord S