Step | Hyp | Ref
| Expression |
1 | | ovex 7395 |
. 2
⊢
(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩) ∈
V |
2 | | c0ex 11156 |
. . . . . . . 8
⊢ 0 ∈
V |
3 | 2 | isseti 3463 |
. . . . . . 7
⊢
∃𝑘 𝑘 = 0 |
4 | | 0z 12517 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
5 | | ccat2s1len 14518 |
. . . . . . . . . . . . . . 15
⊢
(♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) =
2 |
6 | 5 | oveq1i 7372 |
. . . . . . . . . . . . . 14
⊢
((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) − 1) = (2
− 1) |
7 | | 2m1e1 12286 |
. . . . . . . . . . . . . 14
⊢ (2
− 1) = 1 |
8 | 6, 7 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢
((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) − 1) =
1 |
9 | | 1z 12540 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
10 | 8, 9 | eqeltri 2834 |
. . . . . . . . . . . 12
⊢
((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) − 1)
∈ ℤ |
11 | | 0lt1 11684 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
12 | 11, 8 | breqtrri 5137 |
. . . . . . . . . . . 12
⊢ 0 <
((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1) |
13 | | fzolb 13585 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) − 1))
↔ (0 ∈ ℤ ∧ ((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) − 1)
∈ ℤ ∧ 0 < ((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1))) |
14 | 4, 10, 12, 13 | mpbir3an 1342 |
. . . . . . . . . . 11
⊢ 0 ∈
(0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1)) |
15 | | eleq1a 2833 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) − 1))
→ (𝑘 = 0 → 𝑘 ∈
(0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1)))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → 𝑘 ∈
(0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1))) |
17 | | fveq2 6847 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (♯‘𝑏) =
(♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩))) |
18 | 17 | oveq1d 7377 |
. . . . . . . . . . . 12
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ((♯‘𝑏) − 1) =
((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1)) |
19 | 18 | oveq2d 7378 |
. . . . . . . . . . 11
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) →
(0..^((♯‘𝑏)
− 1)) = (0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1))) |
20 | 19 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑘 ∈ (0..^((♯‘𝑏) − 1)) ↔ 𝑘 ∈
(0..^((♯‘(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)) −
1)))) |
21 | 16, 20 | syl5ibr 246 |
. . . . . . . . 9
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑘 = 0 → 𝑘 ∈ (0..^((♯‘𝑏) − 1)))) |
22 | | et-ltneverrefl 45186 |
. . . . . . . . . . 11
⊢ ¬
𝐴 < 𝐴 |
23 | | fveq1 6846 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑏‘0) = ((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘0)) |
24 | | tworepnotupword.1 |
. . . . . . . . . . . . . 14
⊢ 𝐴 ∈ V |
25 | | ccat2s1p1 14524 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V →
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘0) = 𝐴) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘0) = 𝐴 |
27 | 23, 26 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑏‘0) = 𝐴) |
28 | | fveq1 6846 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑏‘(0 + 1)) = ((⟨“𝐴”⟩ ++
⟨“𝐴”⟩)‘(0 +
1))) |
29 | | 1e0p1 12667 |
. . . . . . . . . . . . . . 15
⊢ 1 = (0 +
1) |
30 | 29 | fveq2i 6850 |
. . . . . . . . . . . . . 14
⊢
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘1) =
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘(0 +
1)) |
31 | | ccat2s1p2 14525 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ V →
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘1) = 𝐴) |
32 | 24, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘1) = 𝐴 |
33 | 30, 32 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢
((⟨“𝐴”⟩ ++ ⟨“𝐴”⟩)‘(0 + 1)) =
𝐴 |
34 | 28, 33 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑏‘(0 + 1)) = 𝐴) |
35 | 27, 34 | breq12d 5123 |
. . . . . . . . . . 11
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ((𝑏‘0) < (𝑏‘(0 + 1)) ↔ 𝐴 < 𝐴)) |
36 | 22, 35 | mtbiri 327 |
. . . . . . . . . 10
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ¬ (𝑏‘0) < (𝑏‘(0 +
1))) |
37 | | fveq2 6847 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑏‘𝑘) = (𝑏‘0)) |
38 | | fvoveq1 7385 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑏‘(𝑘 + 1)) = (𝑏‘(0 + 1))) |
39 | 37, 38 | breq12d 5123 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((𝑏‘𝑘) < (𝑏‘(𝑘 + 1)) ↔ (𝑏‘0) < (𝑏‘(0 + 1)))) |
40 | 39 | biimpd 228 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑏‘𝑘) < (𝑏‘(𝑘 + 1)) → (𝑏‘0) < (𝑏‘(0 + 1)))) |
41 | 40 | con3d 152 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (¬ (𝑏‘0) < (𝑏‘(0 + 1)) → ¬
(𝑏‘𝑘) < (𝑏‘(𝑘 + 1)))) |
42 | 36, 41 | syl5com 31 |
. . . . . . . . 9
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑘 = 0 → ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1)))) |
43 | 21, 42 | jcad 514 |
. . . . . . . 8
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑘 = 0 → (𝑘 ∈ (0..^((♯‘𝑏) − 1)) ∧ ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))))) |
44 | 43 | eximdv 1921 |
. . . . . . 7
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (∃𝑘 𝑘 = 0 → ∃𝑘(𝑘 ∈ (0..^((♯‘𝑏) − 1)) ∧ ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))))) |
45 | 3, 44 | mpi 20 |
. . . . . 6
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ∃𝑘(𝑘 ∈ (0..^((♯‘𝑏) − 1)) ∧ ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1)))) |
46 | | nfre1 3271 |
. . . . . . 7
⊢
Ⅎ𝑘∃𝑘 ∈
(0..^((♯‘𝑏)
− 1)) ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1)) |
47 | | rspe 3235 |
. . . . . . 7
⊢ ((𝑘 ∈
(0..^((♯‘𝑏)
− 1)) ∧ ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) → ∃𝑘 ∈ (0..^((♯‘𝑏) − 1)) ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) |
48 | 46, 47 | exlimi 2211 |
. . . . . 6
⊢
(∃𝑘(𝑘 ∈
(0..^((♯‘𝑏)
− 1)) ∧ ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) → ∃𝑘 ∈ (0..^((♯‘𝑏) − 1)) ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) |
49 | 45, 48 | syl 17 |
. . . . 5
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ∃𝑘 ∈
(0..^((♯‘𝑏)
− 1)) ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) |
50 | | rexnal 3104 |
. . . . 5
⊢
(∃𝑘 ∈
(0..^((♯‘𝑏)
− 1)) ¬ (𝑏‘𝑘) < (𝑏‘(𝑘 + 1)) ↔ ¬ ∀𝑘 ∈
(0..^((♯‘𝑏)
− 1))(𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) |
51 | 49, 50 | sylib 217 |
. . . 4
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ¬ ∀𝑘 ∈
(0..^((♯‘𝑏)
− 1))(𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) |
52 | | df-upword 45192 |
. . . . . 6
⊢ UpWord
𝑆 = {𝑏 ∣ (𝑏 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑏) − 1))(𝑏‘𝑘) < (𝑏‘(𝑘 + 1)))} |
53 | 52 | eqabi 2882 |
. . . . 5
⊢ (𝑏 ∈ UpWord 𝑆 ↔ (𝑏 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑏) − 1))(𝑏‘𝑘) < (𝑏‘(𝑘 + 1)))) |
54 | 53 | simprbi 498 |
. . . 4
⊢ (𝑏 ∈ UpWord 𝑆 → ∀𝑘 ∈ (0..^((♯‘𝑏) − 1))(𝑏‘𝑘) < (𝑏‘(𝑘 + 1))) |
55 | 51, 54 | nsyl 140 |
. . 3
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ¬ 𝑏 ∈ UpWord 𝑆) |
56 | | eleq1 2826 |
. . 3
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → (𝑏 ∈ UpWord 𝑆 ↔ (⟨“𝐴”⟩ ++ ⟨“𝐴”⟩) ∈ UpWord
𝑆)) |
57 | 55, 56 | mtbid 324 |
. 2
⊢ (𝑏 = (⟨“𝐴”⟩ ++
⟨“𝐴”⟩) → ¬
(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩) ∈ UpWord
𝑆) |
58 | 1, 57 | vtocle 3547 |
1
⊢ ¬
(⟨“𝐴”⟩ ++ ⟨“𝐴”⟩) ∈ UpWord
𝑆 |