Step | Hyp | Ref
| Expression |
1 | | lencl 13179 |
. . 3
⊢ (𝐴 ∈ Word 𝐵 → (#‘𝐴) ∈
ℕ0) |
2 | | eqeq2 2621 |
. . . . . 6
⊢ (𝑛 = 0 → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = 0)) |
3 | 2 | imbi1d 330 |
. . . . 5
⊢ (𝑛 = 0 → (((#‘𝑥) = 𝑛 → 𝜑) ↔ ((#‘𝑥) = 0 → 𝜑))) |
4 | 3 | ralbidv 2969 |
. . . 4
⊢ (𝑛 = 0 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛 → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = 0 → 𝜑))) |
5 | | eqeq2 2621 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = 𝑚)) |
6 | 5 | imbi1d 330 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((#‘𝑥) = 𝑛 → 𝜑) ↔ ((#‘𝑥) = 𝑚 → 𝜑))) |
7 | 6 | ralbidv 2969 |
. . . 4
⊢ (𝑛 = 𝑚 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛 → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑚 → 𝜑))) |
8 | | eqeq2 2621 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = (𝑚 + 1))) |
9 | 8 | imbi1d 330 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (((#‘𝑥) = 𝑛 → 𝜑) ↔ ((#‘𝑥) = (𝑚 + 1) → 𝜑))) |
10 | 9 | ralbidv 2969 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛 → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑))) |
11 | | eqeq2 2621 |
. . . . . 6
⊢ (𝑛 = (#‘𝐴) → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = (#‘𝐴))) |
12 | 11 | imbi1d 330 |
. . . . 5
⊢ (𝑛 = (#‘𝐴) → (((#‘𝑥) = 𝑛 → 𝜑) ↔ ((#‘𝑥) = (#‘𝐴) → 𝜑))) |
13 | 12 | ralbidv 2969 |
. . . 4
⊢ (𝑛 = (#‘𝐴) → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛 → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑))) |
14 | | hasheq0 13015 |
. . . . . 6
⊢ (𝑥 ∈ Word 𝐵 → ((#‘𝑥) = 0 ↔ 𝑥 = ∅)) |
15 | | wrdind.5 |
. . . . . . 7
⊢ 𝜓 |
16 | | wrdind.1 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
17 | 15, 16 | mpbiri 247 |
. . . . . 6
⊢ (𝑥 = ∅ → 𝜑) |
18 | 14, 17 | syl6bi 242 |
. . . . 5
⊢ (𝑥 ∈ Word 𝐵 → ((#‘𝑥) = 0 → 𝜑)) |
19 | 18 | rgen 2906 |
. . . 4
⊢
∀𝑥 ∈
Word 𝐵((#‘𝑥) = 0 → 𝜑) |
20 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
21 | 20 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((#‘𝑥) = 𝑚 ↔ (#‘𝑦) = 𝑚)) |
22 | | wrdind.2 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
23 | 21, 22 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((#‘𝑥) = 𝑚 → 𝜑) ↔ ((#‘𝑦) = 𝑚 → 𝜒))) |
24 | 23 | cbvralv 3147 |
. . . . 5
⊢
(∀𝑥 ∈
Word 𝐵((#‘𝑥) = 𝑚 → 𝜑) ↔ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚 → 𝜒)) |
25 | | swrdcl 13271 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Word 𝐵 → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝐵) |
26 | 25 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝐵) |
27 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚 → 𝜒)) |
28 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ∈ Word 𝐵) |
29 | | fzossfz 12357 |
. . . . . . . . . . . . . 14
⊢
(0..^(#‘𝑥))
⊆ (0...(#‘𝑥)) |
30 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘𝑥) = (𝑚 + 1)) |
31 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) |
32 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑚 + 1) ∈ ℕ) |
33 | 30, 32 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘𝑥) ∈ ℕ) |
34 | | fzo0end 12426 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑥) ∈
ℕ → ((#‘𝑥)
− 1) ∈ (0..^(#‘𝑥))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) − 1) ∈ (0..^(#‘𝑥))) |
36 | 29, 35 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) − 1) ∈ (0...(#‘𝑥))) |
37 | | swrd0len 13274 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Word 𝐵 ∧ ((#‘𝑥) − 1) ∈ (0...(#‘𝑥))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) =
((#‘𝑥) −
1)) |
38 | 28, 36, 37 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = ((#‘𝑥) − 1)) |
39 | 30 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) − 1) = ((𝑚 + 1) − 1)) |
40 | | nn0cn 11179 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
41 | 40 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑚 ∈ ℂ) |
42 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
43 | | pncan 10166 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑚 + 1)
− 1) = 𝑚) |
44 | 41, 42, 43 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((𝑚 + 1) − 1) = 𝑚) |
45 | 38, 39, 44 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚) |
46 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (#‘𝑦) = (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉))) |
47 | 46 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ((#‘𝑦) = 𝑚 ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚)) |
48 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
49 | 48, 22 | sbcie 3437 |
. . . . . . . . . . . . . 14
⊢
([𝑦 / 𝑥]𝜑 ↔ 𝜒) |
50 | | dfsbcq 3404 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ([𝑦 / 𝑥]𝜑 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑)) |
51 | 49, 50 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (𝜒 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑)) |
52 | 47, 51 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (((#‘𝑦) = 𝑚 → 𝜒) ↔ ((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚 → [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑))) |
53 | 52 | rspcv 3278 |
. . . . . . . . . . 11
⊢ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word
𝐵 → (∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚 → 𝜒) → ((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚 → [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑))) |
54 | 26, 27, 45, 53 | syl3c 64 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑) |
55 | 33 | nnge1d 10940 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 1 ≤ (#‘𝑥)) |
56 | | wrdlenge1n0 13195 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ Word 𝐵 → (𝑥 ≠ ∅ ↔ 1 ≤ (#‘𝑥))) |
57 | 56 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑥 ≠ ∅ ↔ 1 ≤ (#‘𝑥))) |
58 | 55, 57 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ≠ ∅) |
59 | | lswcl 13208 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Word 𝐵 ∧ 𝑥 ≠ ∅) → ( lastS ‘𝑥) ∈ 𝐵) |
60 | 28, 58, 59 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ( lastS ‘𝑥) ∈ 𝐵) |
61 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (𝑦 ++ 〈“𝑧”〉) = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“𝑧”〉)) |
62 | 61 | sbceq1d 3407 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ([(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“𝑧”〉) / 𝑥]𝜑)) |
63 | 50, 62 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (([𝑦 / 𝑥]𝜑 → [(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑) ↔ ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑 → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“𝑧”〉) / 𝑥]𝜑))) |
64 | | s1eq 13233 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ( lastS ‘𝑥) → 〈“𝑧”〉 = 〈“(
lastS ‘𝑥)”〉) |
65 | 64 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ( lastS ‘𝑥) → ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“𝑧”〉) = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“( lastS ‘𝑥)”〉)) |
66 | 65 | sbceq1d 3407 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ( lastS ‘𝑥) → ([((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“𝑧”〉) / 𝑥]𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥]𝜑)) |
67 | 66 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑧 = ( lastS ‘𝑥) → (([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑 → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“𝑧”〉) / 𝑥]𝜑) ↔ ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑 → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥]𝜑))) |
68 | | wrdind.6 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝜒 → 𝜃)) |
69 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ++ 〈“𝑧”〉) ∈
V |
70 | | wrdind.3 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝜑 ↔ 𝜃)) |
71 | 69, 70 | sbcie 3437 |
. . . . . . . . . . . . 13
⊢
([(𝑦 ++
〈“𝑧”〉) / 𝑥]𝜑 ↔ 𝜃) |
72 | 68, 49, 71 | 3imtr4g 284 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → ([𝑦 / 𝑥]𝜑 → [(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑)) |
73 | 63, 67, 72 | vtocl2ga 3247 |
. . . . . . . . . . 11
⊢ (((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word
𝐵 ∧ ( lastS
‘𝑥) ∈ 𝐵) → ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑 → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥]𝜑)) |
74 | 26, 60, 73 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥]𝜑 → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥]𝜑)) |
75 | 54, 74 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥]𝜑) |
76 | | wrdfin 13178 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ Word 𝐵 → 𝑥 ∈ Fin) |
77 | 76 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ∈ Fin) |
78 | | hashnncl 13018 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Fin →
((#‘𝑥) ∈ ℕ
↔ 𝑥 ≠
∅)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅)) |
80 | 33, 79 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ≠ ∅) |
81 | | swrdccatwrd 13320 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Word 𝐵 ∧ 𝑥 ≠ ∅) → ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) =
𝑥) |
82 | 81 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Word 𝐵 ∧ 𝑥 ≠ ∅) → 𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉)) |
83 | 28, 80, 82 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉)) |
84 | | sbceq1a 3413 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉)
→ (𝜑 ↔
[((𝑥 substr 〈0,
((#‘𝑥) −
1)〉) ++ 〈“( lastS ‘𝑥)”〉) / 𝑥]𝜑)) |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥]𝜑)) |
86 | 75, 85 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝜑) |
87 | 86 | expr 641 |
. . . . . . 7
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) ∧ 𝑥 ∈ Word 𝐵) → ((#‘𝑥) = (𝑚 + 1) → 𝜑)) |
88 | 87 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((#‘𝑦) = 𝑚 → 𝜒)) → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑)) |
89 | 88 | ex 449 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
→ (∀𝑦 ∈
Word 𝐵((#‘𝑦) = 𝑚 → 𝜒) → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑))) |
90 | 24, 89 | syl5bi 231 |
. . . 4
⊢ (𝑚 ∈ ℕ0
→ (∀𝑥 ∈
Word 𝐵((#‘𝑥) = 𝑚 → 𝜑) → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑))) |
91 | 4, 7, 10, 13, 19, 90 | nn0ind 11348 |
. . 3
⊢
((#‘𝐴) ∈
ℕ0 → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑)) |
92 | 1, 91 | syl 17 |
. 2
⊢ (𝐴 ∈ Word 𝐵 → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑)) |
93 | | eqidd 2611 |
. 2
⊢ (𝐴 ∈ Word 𝐵 → (#‘𝐴) = (#‘𝐴)) |
94 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴)) |
95 | 94 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 𝐴 → ((#‘𝑥) = (#‘𝐴) ↔ (#‘𝐴) = (#‘𝐴))) |
96 | | wrdind.4 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
97 | 95, 96 | imbi12d 333 |
. . 3
⊢ (𝑥 = 𝐴 → (((#‘𝑥) = (#‘𝐴) → 𝜑) ↔ ((#‘𝐴) = (#‘𝐴) → 𝜏))) |
98 | 97 | rspcv 3278 |
. 2
⊢ (𝐴 ∈ Word 𝐵 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑) → ((#‘𝐴) = (#‘𝐴) → 𝜏))) |
99 | 92, 93, 98 | mp2d 47 |
1
⊢ (𝐴 ∈ Word 𝐵 → 𝜏) |