Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑋 → (#‘𝐴) ∈
ℕ0) |
2 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑛 = 0 → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = 0)) |
3 | 2 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑛 = 0 → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) ↔ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 0))) |
4 | 3 | imbi1d 331 |
. . . . . . 7
⊢ (𝑛 = 0 → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 0) → 𝜑))) |
5 | 4 | 2ralbidv 2989 |
. . . . . 6
⊢ (𝑛 = 0 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 0) → 𝜑))) |
6 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = 𝑚)) |
7 | 6 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) ↔ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚))) |
8 | 7 | imbi1d 331 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑))) |
9 | 8 | 2ralbidv 2989 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑))) |
10 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑛 = (𝑚 + 1) → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = (𝑚 + 1))) |
11 | 10 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) ↔ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) |
12 | 11 | imbi1d 331 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)) → 𝜑))) |
13 | 12 | 2ralbidv 2989 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)) → 𝜑))) |
14 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑛 = (#‘𝐴) → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = (#‘𝐴))) |
15 | 14 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑛 = (#‘𝐴) → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) ↔ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)))) |
16 | 15 | imbi1d 331 |
. . . . . . 7
⊢ (𝑛 = (#‘𝐴) → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑))) |
17 | 16 | 2ralbidv 2989 |
. . . . . 6
⊢ (𝑛 = (#‘𝐴) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑))) |
18 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢
((#‘𝑥) = 0
→ ((#‘𝑥) =
(#‘𝑤) ↔ 0 =
(#‘𝑤))) |
19 | 18 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (#‘𝑥) = 0) → ((#‘𝑥) = (#‘𝑤) ↔ 0 = (#‘𝑤))) |
20 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
⊢ (0 =
(#‘𝑤) ↔
(#‘𝑤) =
0) |
21 | | hasheq0 13154 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Word 𝑌 → ((#‘𝑤) = 0 ↔ 𝑤 = ∅)) |
22 | 20, 21 | syl5bb 272 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ Word 𝑌 → (0 = (#‘𝑤) ↔ 𝑤 = ∅)) |
23 | | hasheq0 13154 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word 𝑋 → ((#‘𝑥) = 0 ↔ 𝑥 = ∅)) |
24 | | wrd2ind.6 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝜓 |
25 | | wrd2ind.1 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → (𝜑 ↔ 𝜓)) |
26 | 24, 25 | mpbiri 248 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → 𝜑) |
27 | 26 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (𝑤 = ∅ → 𝜑)) |
28 | 23, 27 | syl6bi 243 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ Word 𝑋 → ((#‘𝑥) = 0 → (𝑤 = ∅ → 𝜑))) |
29 | 28 | com13 88 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∅ →
((#‘𝑥) = 0 →
(𝑥 ∈ Word 𝑋 → 𝜑))) |
30 | 22, 29 | syl6bi 243 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Word 𝑌 → (0 = (#‘𝑤) → ((#‘𝑥) = 0 → (𝑥 ∈ Word 𝑋 → 𝜑)))) |
31 | 30 | com24 95 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ Word 𝑌 → (𝑥 ∈ Word 𝑋 → ((#‘𝑥) = 0 → (0 = (#‘𝑤) → 𝜑)))) |
32 | 31 | imp31 448 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (#‘𝑥) = 0) → (0 = (#‘𝑤) → 𝜑)) |
33 | 19, 32 | sylbid 230 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (#‘𝑥) = 0) → ((#‘𝑥) = (#‘𝑤) → 𝜑)) |
34 | 33 | ex 450 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → ((#‘𝑥) = 0 → ((#‘𝑥) = (#‘𝑤) → 𝜑))) |
35 | 34 | com23 86 |
. . . . . . . 8
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → ((#‘𝑥) = (#‘𝑤) → ((#‘𝑥) = 0 → 𝜑))) |
36 | 35 | impd 447 |
. . . . . . 7
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 0) → 𝜑)) |
37 | 36 | rgen2 2975 |
. . . . . 6
⊢
∀𝑤 ∈
Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 0) → 𝜑) |
38 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
39 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → (#‘𝑤) = (#‘𝑢)) |
40 | 38, 39 | eqeqan12d 2638 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((#‘𝑥) = (#‘𝑤) ↔ (#‘𝑦) = (#‘𝑢))) |
41 | 38 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((#‘𝑥) = 𝑚 ↔ (#‘𝑦) = 𝑚)) |
42 | 41 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((#‘𝑥) = 𝑚 ↔ (#‘𝑦) = 𝑚)) |
43 | 40, 42 | anbi12d 747 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) ↔ ((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚))) |
44 | | wrd2ind.2 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (𝜑 ↔ 𝜒)) |
45 | 43, 44 | imbi12d 334 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑) ↔ (((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒))) |
46 | 45 | ancoms 469 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑢 ∧ 𝑥 = 𝑦) → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑) ↔ (((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒))) |
47 | 46 | cbvraldva 3177 |
. . . . . . . 8
⊢ (𝑤 = 𝑢 → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑) ↔ ∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒))) |
48 | 47 | cbvralv 3171 |
. . . . . . 7
⊢
(∀𝑤 ∈
Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑) ↔ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) |
49 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Word 𝑌 → (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word 𝑌) |
50 | 49 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word 𝑌) |
51 | 50 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word 𝑌) |
52 | | simprll 802 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Word 𝑌) |
53 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑥) =
(𝑚 + 1) →
((#‘𝑥) =
(#‘𝑤) ↔ (𝑚 + 1) = (#‘𝑤))) |
54 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) |
55 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑤) =
(𝑚 + 1) →
((#‘𝑤) ∈ ℕ
↔ (𝑚 + 1) ∈
ℕ)) |
56 | 55 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 + 1) = (#‘𝑤) → ((#‘𝑤) ∈ ℕ ↔ (𝑚 + 1) ∈
ℕ)) |
57 | 54, 56 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 + 1) = (#‘𝑤) → (𝑚 ∈ ℕ0 →
(#‘𝑤) ∈
ℕ)) |
58 | 53, 57 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑥) =
(𝑚 + 1) →
((#‘𝑥) =
(#‘𝑤) → (𝑚 ∈ ℕ0
→ (#‘𝑤) ∈
ℕ))) |
59 | 58 | impcom 446 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑥) =
(#‘𝑤) ∧
(#‘𝑥) = (𝑚 + 1)) → (𝑚 ∈ ℕ0
→ (#‘𝑤) ∈
ℕ)) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑚 ∈ ℕ0 →
(#‘𝑤) ∈
ℕ)) |
61 | 60 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑤) ∈ ℕ) |
62 | 61 | nnge1d 11063 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 1 ≤ (#‘𝑤)) |
63 | | wrdlenge1n0 13340 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ Word 𝑌 → (𝑤 ≠ ∅ ↔ 1 ≤ (#‘𝑤))) |
64 | 52, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝑤 ≠ ∅ ↔ 1 ≤ (#‘𝑤))) |
65 | 62, 64 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑤 ≠ ∅) |
66 | | lswcl 13355 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → ( lastS ‘𝑤) ∈ 𝑌) |
67 | 52, 65, 66 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ( lastS ‘𝑤) ∈ 𝑌) |
68 | 51, 67 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word 𝑌 ∧ ( lastS ‘𝑤) ∈ 𝑌)) |
69 | | swrdcl 13419 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word 𝑋 → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝑋) |
70 | 69 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝑋) |
71 | 70 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝑋) |
72 | | simprlr 803 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Word 𝑋) |
73 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑥) =
(𝑚 + 1) →
((#‘𝑥) ∈ ℕ
↔ (𝑚 + 1) ∈
ℕ)) |
74 | 54, 73 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑥) =
(𝑚 + 1) → (𝑚 ∈ ℕ0
→ (#‘𝑥) ∈
ℕ)) |
75 | 74 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑚 ∈ ℕ0 →
(#‘𝑥) ∈
ℕ)) |
76 | 75 | impcom 446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑥) ∈ ℕ) |
77 | 76 | nnge1d 11063 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 1 ≤ (#‘𝑥)) |
78 | | wrdlenge1n0 13340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ Word 𝑋 → (𝑥 ≠ ∅ ↔ 1 ≤ (#‘𝑥))) |
79 | 72, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝑥 ≠ ∅ ↔ 1 ≤ (#‘𝑥))) |
80 | 77, 79 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑥 ≠ ∅) |
81 | | lswcl 13355 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → ( lastS ‘𝑥) ∈ 𝑋) |
82 | 72, 80, 81 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ( lastS ‘𝑥) ∈ 𝑋) |
83 | 68, 71, 82 | jca32 558 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word 𝑌 ∧ ( lastS ‘𝑤) ∈ 𝑌) ∧ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝑋 ∧ ( lastS ‘𝑥) ∈ 𝑋))) |
84 | 83 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word 𝑌 ∧ ( lastS ‘𝑤) ∈ 𝑌) ∧ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝑋 ∧ ( lastS ‘𝑥) ∈ 𝑋))) |
85 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋)) |
86 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) |
87 | | simprrl 804 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑥) = (#‘𝑤)) |
88 | 87 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑥) − 1) = ((#‘𝑤) − 1)) |
89 | | simprlr 803 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Word 𝑋) |
90 | | fzossfz 12488 |
. . . . . . . . . . . . . . . . . 18
⊢
(0..^(#‘𝑥))
⊆ (0...(#‘𝑥)) |
91 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑥) = (𝑚 + 1)) |
92 | 54 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝑚 + 1) ∈ ℕ) |
93 | 91, 92 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑥) ∈ ℕ) |
94 | | fzo0end 12560 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑥) ∈
ℕ → ((#‘𝑥)
− 1) ∈ (0..^(#‘𝑥))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑥) − 1) ∈ (0..^(#‘𝑥))) |
96 | 90, 95 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑥) − 1) ∈ (0...(#‘𝑥))) |
97 | | swrd0len 13422 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word 𝑋 ∧ ((#‘𝑥) − 1) ∈ (0...(#‘𝑥))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) =
((#‘𝑥) −
1)) |
98 | 89, 96, 97 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = ((#‘𝑥) − 1)) |
99 | | simprll 802 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Word 𝑌) |
100 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑤) =
(#‘𝑥) →
((#‘𝑤) − 1) =
((#‘𝑥) −
1)) |
101 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑤) =
(#‘𝑥) →
(0...(#‘𝑤)) =
(0...(#‘𝑥))) |
102 | 100, 101 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑤) =
(#‘𝑥) →
(((#‘𝑤) − 1)
∈ (0...(#‘𝑤))
↔ ((#‘𝑥) −
1) ∈ (0...(#‘𝑥)))) |
103 | 102 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑥) =
(#‘𝑤) →
(((#‘𝑤) − 1)
∈ (0...(#‘𝑤))
↔ ((#‘𝑥) −
1) ∈ (0...(#‘𝑥)))) |
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑥) =
(#‘𝑤) ∧
(#‘𝑥) = (𝑚 + 1)) → (((#‘𝑤) − 1) ∈
(0...(#‘𝑤)) ↔
((#‘𝑥) − 1)
∈ (0...(#‘𝑥)))) |
105 | 104 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (((#‘𝑤) − 1) ∈ (0...(#‘𝑤)) ↔ ((#‘𝑥) − 1) ∈
(0...(#‘𝑥)))) |
106 | 96, 105 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑤) − 1) ∈ (0...(#‘𝑤))) |
107 | | swrd0len 13422 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Word 𝑌 ∧ ((#‘𝑤) − 1) ∈ (0...(#‘𝑤))) → (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) =
((#‘𝑤) −
1)) |
108 | 99, 106, 107 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) = ((#‘𝑤) − 1)) |
109 | 88, 98, 108 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉))) |
110 | 91 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑥) − 1) = ((𝑚 + 1) − 1)) |
111 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
112 | 111 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑚 ∈ ℂ) |
113 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
114 | | pncan 10287 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑚 + 1)
− 1) = 𝑚) |
115 | 112, 113,
114 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((𝑚 + 1) − 1) = 𝑚) |
116 | 98, 110, 115 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚) |
117 | 109, 116 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧
(#‘(𝑥 substr 〈0,
((#‘𝑥) −
1)〉)) = 𝑚)) |
118 | 70 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word
𝑋) |
119 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (#‘𝑦) = (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉))) |
120 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → (#‘𝑢) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) |
121 | 119, 120 | eqeqan12d 2638 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) → ((#‘𝑦) = (#‘𝑢) ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉)))) |
122 | 121 | expcom 451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ((#‘𝑦) = (#‘𝑢) ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉))))) |
123 | 122 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) → (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ((#‘𝑦) = (#‘𝑢) ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉))))) |
124 | 123 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → ((#‘𝑦) = (#‘𝑢) ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉)))) |
125 | 119 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ((#‘𝑦) = 𝑚 ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚)) |
126 | 125 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → ((#‘𝑦) = 𝑚 ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = 𝑚)) |
127 | 124, 126 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → (((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) ↔ ((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧
(#‘(𝑥 substr 〈0,
((#‘𝑥) −
1)〉)) = 𝑚))) |
128 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
129 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑢 ∈ V |
130 | 128, 129,
44 | sbc2ie 3505 |
. . . . . . . . . . . . . . . . . . . 20
⊢
([𝑦 / 𝑥][𝑢 / 𝑤]𝜑 ↔ 𝜒) |
131 | 130 | bicomi 214 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 ↔ [𝑦 / 𝑥][𝑢 / 𝑤]𝜑) |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → (𝜒 ↔ [𝑦 / 𝑥][𝑢 / 𝑤]𝜑)) |
133 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) |
134 | 133 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → ([𝑦 / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][𝑢 / 𝑤]𝜑)) |
135 | | dfsbcq 3437 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ([𝑢 / 𝑤]𝜑 ↔ [(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
136 | 135 | sbcbidv 3490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) → ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
138 | 137 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
139 | 132, 134,
138 | 3bitrd 294 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → (𝜒 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
140 | 127, 139 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧ 𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) → ((((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒) ↔ (((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧
(#‘(𝑥 substr 〈0,
((#‘𝑥) −
1)〉)) = 𝑚) →
[(𝑥 substr 〈0,
((#‘𝑥) −
1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑))) |
141 | 118, 140 | rspcdv 3312 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) → (∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒) → (((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧
(#‘(𝑥 substr 〈0,
((#‘𝑥) −
1)〉)) = 𝑚) →
[(𝑥 substr 〈0,
((#‘𝑥) −
1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑))) |
142 | 50, 141 | rspcimdv 3310 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒) → (((#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ∧
(#‘(𝑥 substr 〈0,
((#‘𝑥) −
1)〉)) = 𝑚) →
[(𝑥 substr 〈0,
((#‘𝑥) −
1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑))) |
143 | 85, 86, 117, 142 | syl3c 66 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑) |
144 | 143, 109 | jca 554 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉)))) |
145 | | dfsbcq 3437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ [(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤][𝑦 / 𝑥]𝜑)) |
146 | | sbccom 3509 |
. . . . . . . . . . . . . . . 16
⊢
([(𝑤 substr
〈0, ((#‘𝑤)
− 1)〉) / 𝑤][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑) |
147 | 145, 146 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
148 | 120 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ((#‘𝑦) = (#‘𝑢) ↔ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)))) |
149 | 147, 148 | anbi12d 747 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → (([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (#‘𝑦) = (#‘𝑢)) ↔ ([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))))) |
150 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → (𝑢 ++ 〈“𝑠”〉) = ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“𝑠”〉)) |
151 | 150 | sbceq1d 3440 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ([(𝑢 ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑 ↔ [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑)) |
152 | 149, 151 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) → ((([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (#‘𝑦) = (#‘𝑢)) → [(𝑢 ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑))) |
153 | | s1eq 13380 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = ( lastS ‘𝑤) → 〈“𝑠”〉 = 〈“(
lastS ‘𝑤)”〉) |
154 | 153 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = ( lastS ‘𝑤) → ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“𝑠”〉) = ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉)) |
155 | 154 | sbceq1d 3440 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = ( lastS ‘𝑤) → ([((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑 ↔ [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑)) |
156 | 155 | imbi2d 330 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = ( lastS ‘𝑤) → ((([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑))) |
157 | | sbccom 3509 |
. . . . . . . . . . . . . . . 16
⊢
([((𝑤 substr
〈0, ((#‘𝑤)
− 1)〉) ++ 〈“( lastS ‘𝑤)”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑 ↔ [(𝑦 ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑) |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = ( lastS ‘𝑤) → ([((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑 ↔ [(𝑦 ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑)) |
159 | 158 | imbi2d 330 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = ( lastS ‘𝑤) → ((([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [(𝑦 ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑))) |
160 | 156, 159 | bitrd 268 |
. . . . . . . . . . . . 13
⊢ (𝑠 = ( lastS ‘𝑤) → ((([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [(𝑦 ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑))) |
161 | | dfsbcq 3437 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ↔ [(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑)) |
162 | 119 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ((#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉)) ↔ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) =
(#‘(𝑤 substr 〈0,
((#‘𝑤) −
1)〉)))) |
163 | 161, 162 | anbi12d 747 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) ↔ ([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) −
1)〉))))) |
164 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → (𝑦 ++ 〈“𝑧”〉) = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“𝑧”〉)) |
165 | 164 | sbceq1d 3440 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ([(𝑦 ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑)) |
166 | 163, 165 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) → ((([𝑦 / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘𝑦) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) → [(𝑦 ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑) ↔ (([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) →
[((𝑥 substr 〈0,
((#‘𝑥) −
1)〉) ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑))) |
167 | | s1eq 13380 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ( lastS ‘𝑥) → 〈“𝑧”〉 = 〈“(
lastS ‘𝑥)”〉) |
168 | 167 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ( lastS ‘𝑥) → ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“𝑧”〉) = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“( lastS ‘𝑥)”〉)) |
169 | 168 | sbceq1d 3440 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ( lastS ‘𝑥) → ([((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑)) |
170 | 169 | imbi2d 330 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ( lastS ‘𝑥) → ((([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) →
[((𝑥 substr 〈0,
((#‘𝑥) −
1)〉) ++ 〈“𝑧”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑) ↔ (([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) →
[((𝑥 substr 〈0,
((#‘𝑥) −
1)〉) ++ 〈“( lastS ‘𝑥)”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑))) |
171 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (#‘𝑦) = (#‘𝑢)) → (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) |
172 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (#‘𝑦) = (#‘𝑢)) → (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌)) |
173 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (#‘𝑦) = (#‘𝑢)) → (#‘𝑦) = (#‘𝑢)) |
174 | | wrd2ind.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (#‘𝑦) = (#‘𝑢)) → (𝜒 → 𝜃)) |
175 | 171, 172,
173, 174 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (#‘𝑦) = (#‘𝑢)) → (𝜒 → 𝜃)) |
176 | 44 | ancoms 469 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 = 𝑢 ∧ 𝑥 = 𝑦) → (𝜑 ↔ 𝜒)) |
177 | 129, 128,
176 | sbc2ie 3505 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ 𝜒) |
178 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ++ 〈“𝑠”〉) ∈
V |
179 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ++ 〈“𝑧”〉) ∈
V |
180 | | wrd2ind.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = (𝑦 ++ 〈“𝑧”〉) ∧ 𝑤 = (𝑢 ++ 〈“𝑠”〉)) → (𝜑 ↔ 𝜃)) |
181 | 180 | ancoms 469 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 = (𝑢 ++ 〈“𝑠”〉) ∧ 𝑥 = (𝑦 ++ 〈“𝑧”〉)) → (𝜑 ↔ 𝜃)) |
182 | 178, 179,
181 | sbc2ie 3505 |
. . . . . . . . . . . . . . . . 17
⊢
([(𝑢 ++
〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑 ↔ 𝜃) |
183 | 175, 177,
182 | 3imtr4g 285 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (#‘𝑦) = (#‘𝑢)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → [(𝑢 ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑)) |
184 | 183 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((#‘𝑦) = (#‘𝑢) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → [(𝑢 ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑))) |
185 | 184 | com23 86 |
. . . . . . . . . . . . . 14
⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → ((#‘𝑦) = (#‘𝑢) → [(𝑢 ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑))) |
186 | 185 | impd 447 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → (([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (#‘𝑦) = (#‘𝑢)) → [(𝑢 ++ 〈“𝑠”〉) / 𝑤][(𝑦 ++ 〈“𝑧”〉) / 𝑥]𝜑)) |
187 | 152, 160,
166, 170, 186 | vtocl4ga 3278 |
. . . . . . . . . . . 12
⊢ ((((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ∈ Word
𝑌 ∧ ( lastS
‘𝑤) ∈ 𝑌) ∧ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ∈ Word 𝑋 ∧ ( lastS ‘𝑥) ∈ 𝑋)) → (([(𝑥 substr 〈0, ((#‘𝑥) − 1)〉) / 𝑥][(𝑤 substr 〈0, ((#‘𝑤) − 1)〉) / 𝑤]𝜑 ∧ (#‘(𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) = (#‘(𝑤 substr 〈0, ((#‘𝑤) − 1)〉))) →
[((𝑥 substr 〈0,
((#‘𝑥) −
1)〉) ++ 〈“( lastS ‘𝑥)”〉) / 𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) /
𝑤]𝜑)) |
188 | 84, 144, 187 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑) |
189 | | eqtr2 2642 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑥) =
(#‘𝑤) ∧
(#‘𝑥) = (𝑚 + 1)) → (#‘𝑤) = (𝑚 + 1)) |
190 | 189 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑤) = (𝑚 + 1)) |
191 | 190, 92 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (#‘𝑤) ∈ ℕ) |
192 | | wrdfin 13323 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Word 𝑌 → 𝑤 ∈ Fin) |
193 | 192 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → 𝑤 ∈ Fin) |
194 | 193 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Fin) |
195 | | hashnncl 13157 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Fin →
((#‘𝑤) ∈ ℕ
↔ 𝑤 ≠
∅)) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑤) ∈ ℕ ↔ 𝑤 ≠ ∅)) |
197 | 191, 196 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑤 ≠ ∅) |
198 | | swrdccatwrd 13468 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) =
𝑤) |
199 | 198 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → 𝑤 = ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉)) |
200 | 99, 197, 199 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑤 = ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉)) |
201 | | wrdfin 13323 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ Word 𝑋 → 𝑥 ∈ Fin) |
202 | 201 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → 𝑥 ∈ Fin) |
203 | 202 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Fin) |
204 | | hashnncl 13157 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ Fin →
((#‘𝑥) ∈ ℕ
↔ 𝑥 ≠
∅)) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → ((#‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅)) |
206 | 93, 205 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑥 ≠ ∅) |
207 | | swrdccatwrd 13468 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) =
𝑥) |
208 | 207 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → 𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉)) |
209 | 89, 206, 208 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉)) |
210 | | sbceq1a 3446 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉)
→ (𝜑 ↔
[((𝑤 substr 〈0,
((#‘𝑤) −
1)〉) ++ 〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑)) |
211 | | sbceq1a 3446 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉)
→ ([((𝑤 substr
〈0, ((#‘𝑤)
− 1)〉) ++ 〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑)) |
212 | 210, 211 | sylan9bb 736 |
. . . . . . . . . . . 12
⊢ ((𝑤 = ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉)
∧ 𝑥 = ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++
〈“( lastS ‘𝑥)”〉)) → (𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑)) |
213 | 200, 209,
212 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → (𝜑 ↔ [((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) ++ 〈“( lastS
‘𝑥)”〉) /
𝑥][((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++
〈“( lastS ‘𝑤)”〉) / 𝑤]𝜑)) |
214 | 188, 213 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)))) → 𝜑) |
215 | 214 | expr 643 |
. . . . . . . . 9
⊢ (((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) ∧ (𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋)) → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)) → 𝜑)) |
216 | 215 | ralrimivva 2971 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ ∀𝑢 ∈ Word
𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒)) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)) → 𝜑)) |
217 | 216 | ex 450 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (∀𝑢 ∈
Word 𝑌∀𝑦 ∈ Word 𝑋(((#‘𝑦) = (#‘𝑢) ∧ (#‘𝑦) = 𝑚) → 𝜒) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)) → 𝜑))) |
218 | 48, 217 | syl5bi 232 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ (∀𝑤 ∈
Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = 𝑚) → 𝜑) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (𝑚 + 1)) → 𝜑))) |
219 | 5, 9, 13, 17, 37, 218 | nn0ind 11472 |
. . . . 5
⊢
((#‘𝐴) ∈
ℕ0 → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑)) |
220 | 1, 219 | syl 17 |
. . . 4
⊢ (𝐴 ∈ Word 𝑋 → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑)) |
221 | 220 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑)) |
222 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑤 = 𝐵 → (#‘𝑤) = (#‘𝐵)) |
223 | 222 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑤 = 𝐵 → ((#‘𝑥) = (#‘𝑤) ↔ (#‘𝑥) = (#‘𝐵))) |
224 | 223 | anbi1d 741 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) ↔ ((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)))) |
225 | | wrd2ind.5 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝜑 ↔ 𝜌)) |
226 | 224, 225 | imbi12d 334 |
. . . . . 6
⊢ (𝑤 = 𝐵 → ((((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑) ↔ (((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌))) |
227 | 226 | ralbidv 2986 |
. . . . 5
⊢ (𝑤 = 𝐵 → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑) ↔ ∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌))) |
228 | 227 | rspcv 3305 |
. . . 4
⊢ (𝐵 ∈ Word 𝑌 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑) → ∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌))) |
229 | 228 | 3ad2ant2 1083 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝑤) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜑) → ∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌))) |
230 | 221, 229 | mpd 15 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → ∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌)) |
231 | | eqidd 2623 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → (#‘𝐴) = (#‘𝐴)) |
232 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴)) |
233 | 232 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ((#‘𝑥) = (#‘𝐵) ↔ (#‘𝐴) = (#‘𝐵))) |
234 | 232 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ((#‘𝑥) = (#‘𝐴) ↔ (#‘𝐴) = (#‘𝐴))) |
235 | 233, 234 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) ↔ ((#‘𝐴) = (#‘𝐵) ∧ (#‘𝐴) = (#‘𝐴)))) |
236 | | wrd2ind.4 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝜌 ↔ 𝜏)) |
237 | 235, 236 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) ↔ (((#‘𝐴) = (#‘𝐵) ∧ (#‘𝐴) = (#‘𝐴)) → 𝜏))) |
238 | 237 | rspcv 3305 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑋 → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) → (((#‘𝐴) = (#‘𝐵) ∧ (#‘𝐴) = (#‘𝐴)) → 𝜏))) |
239 | 238 | com23 86 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑋 → (((#‘𝐴) = (#‘𝐵) ∧ (#‘𝐴) = (#‘𝐴)) → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) → 𝜏))) |
240 | 239 | expd 452 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑋 → ((#‘𝐴) = (#‘𝐵) → ((#‘𝐴) = (#‘𝐴) → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) → 𝜏)))) |
241 | 240 | com34 91 |
. . . 4
⊢ (𝐴 ∈ Word 𝑋 → ((#‘𝐴) = (#‘𝐵) → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) → ((#‘𝐴) = (#‘𝐴) → 𝜏)))) |
242 | 241 | imp 445 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ (#‘𝐴) = (#‘𝐵)) → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) → ((#‘𝐴) = (#‘𝐴) → 𝜏))) |
243 | 242 | 3adant2 1080 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → (∀𝑥 ∈ Word 𝑋(((#‘𝑥) = (#‘𝐵) ∧ (#‘𝑥) = (#‘𝐴)) → 𝜌) → ((#‘𝐴) = (#‘𝐴) → 𝜏))) |
244 | 230, 231,
243 | mp2d 49 |
1
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → 𝜏) |