Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. . 3
⊢ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉))) |
2 | | wwlknimp 26215 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸)) |
3 | | simp1 1054 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) → 𝑇 ∈ Word 𝑉) |
4 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → 𝑆 ∈ 𝑉) |
5 | | cats1un 13327 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑇 ++ 〈“𝑆”〉) = (𝑇 ∪ {〈(#‘𝑇), 𝑆〉})) |
6 | 3, 4, 5 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (𝑇 ++ 〈“𝑆”〉) = (𝑇 ∪ {〈(#‘𝑇), 𝑆〉})) |
7 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈(#‘𝑇),
𝑆〉 ∈
V |
8 | 7 | snnz 4252 |
. . . . . . . . . . . . . . . . . . . 20
⊢
{〈(#‘𝑇),
𝑆〉} ≠
∅ |
9 | 8 | neii 2784 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
{〈(#‘𝑇), 𝑆〉} =
∅ |
10 | 9 | intnan 951 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
(𝑇 = ∅ ∧
{〈(#‘𝑇), 𝑆〉} =
∅) |
11 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 ∪ {〈(#‘𝑇), 𝑆〉}) ≠ ∅ ↔ ¬ (𝑇 ∪ {〈(#‘𝑇), 𝑆〉}) = ∅) |
12 | | un00 3963 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 = ∅ ∧
{〈(#‘𝑇), 𝑆〉} = ∅) ↔ (𝑇 ∪ {〈(#‘𝑇), 𝑆〉}) = ∅) |
13 | 11, 12 | xchbinxr 324 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∪ {〈(#‘𝑇), 𝑆〉}) ≠ ∅ ↔ ¬ (𝑇 = ∅ ∧
{〈(#‘𝑇), 𝑆〉} =
∅)) |
14 | 10, 13 | mpbir 220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∪ {〈(#‘𝑇), 𝑆〉}) ≠ ∅ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (𝑇 ∪ {〈(#‘𝑇), 𝑆〉}) ≠ ∅) |
16 | 6, 15 | eqnetrd 2849 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (𝑇 ++ 〈“𝑆”〉) ≠
∅) |
17 | | s1cl 13235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ 𝑉 → 〈“𝑆”〉 ∈ Word 𝑉) |
18 | 17 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → 〈“𝑆”〉 ∈ Word 𝑉) |
19 | | ccatcl 13212 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ Word 𝑉 ∧ 〈“𝑆”〉 ∈ Word 𝑉) → (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉) |
20 | 3, 18, 19 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉) |
21 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑇 ∈ Word 𝑉) |
22 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → 𝑆 ∈ 𝑉) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑆 ∈ 𝑉) |
24 | | fzossfzop1 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
25 | 24 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℕ0
→ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
26 | 25 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
27 | 26 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
28 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝑇) =
(𝑁 + 1) →
(0..^(#‘𝑇)) =
(0..^(𝑁 +
1))) |
29 | 28 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝑇) =
(𝑁 + 1) → (𝑖 ∈ (0..^(#‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^(#‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
31 | 30 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(#‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
32 | 27, 31 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(#‘𝑇))) |
33 | | ccats1val1 13255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝑖 ∈ (0..^(#‘𝑇))) → ((𝑇 ++ 〈“𝑆”〉)‘𝑖) = (𝑇‘𝑖)) |
34 | 21, 23, 32, 33 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ 〈“𝑆”〉)‘𝑖) = (𝑇‘𝑖)) |
35 | 34 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑇‘𝑖) = ((𝑇 ++ 〈“𝑆”〉)‘𝑖)) |
36 | | fzonn0p1p1 12413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
38 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (0..^(#‘𝑇)) = (0..^(𝑁 + 1))) |
39 | 38 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (0..^(#‘𝑇)) = (0..^(𝑁 + 1))) |
40 | 37, 39 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(#‘𝑇))) |
41 | | ccats1val1 13255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑖 + 1) ∈ (0..^(#‘𝑇))) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1))) |
42 | 21, 23, 40, 41 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1))) |
43 | 42 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑇‘(𝑖 + 1)) = ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))) |
44 | 35, 43 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))}) |
45 | 44 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑆 ∈ 𝑉 → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))})))) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))})))) |
47 | 46 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))}))) |
48 | 47 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (𝑖 ∈ (0..^𝑁) → {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))})) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))}) |
50 | 49 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
51 | 50 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
52 | 51 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
53 | 52 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
54 | 53 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
55 | 54 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
56 | 55 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
57 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑇) =
(𝑁 + 1) →
((#‘𝑇) − 1) =
((𝑁 + 1) −
1)) |
58 | 57 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ((#‘𝑇) − 1) = ((𝑁 + 1) − 1)) |
59 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
60 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 1 ∈
ℂ |
61 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
62 | 59, 60, 61 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
63 | 62 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ((𝑁 + 1) − 1) = 𝑁) |
64 | 58, 63 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ((#‘𝑇) − 1) = 𝑁) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → (𝑇‘((#‘𝑇) − 1)) = (𝑇‘𝑁)) |
66 | | lsw 13204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑇 ∈ Word 𝑉 → ( lastS ‘𝑇) = (𝑇‘((#‘𝑇) − 1))) |
67 | 66 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ( lastS ‘𝑇) = (𝑇‘((#‘𝑇) − 1))) |
68 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → 𝑇 ∈ Word 𝑉) |
69 | | fzonn0p1 12411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
70 | 69 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
71 | 28 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑇) =
(𝑁 + 1) → (𝑁 ∈ (0..^(#‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1)))) |
72 | 71 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → (𝑁 ∈ (0..^(#‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1)))) |
73 | 70, 72 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(#‘𝑇))) |
74 | | ccats1val1 13255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑇))) → ((𝑇 ++ 〈“𝑆”〉)‘𝑁) = (𝑇‘𝑁)) |
75 | 68, 22, 73, 74 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ((𝑇 ++ 〈“𝑆”〉)‘𝑁) = (𝑇‘𝑁)) |
76 | 65, 67, 75 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ( lastS ‘𝑇) = ((𝑇 ++ 〈“𝑆”〉)‘𝑁)) |
77 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (#‘𝑇) = (𝑁 + 1)) |
78 | 77 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → (𝑁 + 1) = (#‘𝑇)) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → (𝑁 + 1) = (#‘𝑇)) |
80 | | ccats1val2 13256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (#‘𝑇)) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1)) = 𝑆) |
81 | 68, 22, 79, 80 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1)) = 𝑆) |
82 | 81 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → 𝑆 = ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))) |
83 | 76, 82 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → {( lastS ‘𝑇), 𝑆} = {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))}) |
84 | 83 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → ({( lastS ‘𝑇), 𝑆} ∈ ran 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
85 | 84 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({( lastS
‘𝑇), 𝑆} ∈ ran 𝐸 → (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1))) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
86 | 85 | exp4c 634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({( lastS
‘𝑇), 𝑆} ∈ ran 𝐸 → (𝑆 ∈ 𝑉 → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)))) |
87 | 86 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸))) |
88 | 87 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
89 | 88 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
90 | 89 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
91 | 90 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸) |
92 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑁 → ((𝑇 ++ 〈“𝑆”〉)‘𝑖) = ((𝑇 ++ 〈“𝑆”〉)‘𝑁)) |
93 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 𝑁 → (𝑖 + 1) = (𝑁 + 1)) |
94 | 93 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑁 → ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1)) = ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))) |
95 | 92, 94 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 𝑁 → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))}) |
96 | 95 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑁 → ({((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
97 | 96 | ralsng 4165 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (∀𝑖 ∈
{𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
98 | 97 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (∀𝑖 ∈ {𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
99 | 91, 98 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ∀𝑖 ∈ {𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
100 | | ralunb 3756 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑖 ∈
((0..^𝑁) ∪ {𝑁}){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
101 | 56, 99, 100 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
102 | | elnn0uz 11601 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
103 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
104 | 102, 103 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...𝑁)) |
105 | | fzelp1 12263 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ (0...𝑁) → 𝑁 ∈ (0...(𝑁 + 1))) |
106 | | fzosplit 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ (0...(𝑁 + 1)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1)))) |
107 | 104, 105,
106 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
((0..^𝑁) ∪ (𝑁..^(𝑁 + 1)))) |
108 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
109 | | fzosn 12405 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → (𝑁..^(𝑁 + 1)) = {𝑁}) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁..^(𝑁 + 1)) = {𝑁}) |
111 | 110 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((0..^𝑁) ∪
(𝑁..^(𝑁 + 1))) = ((0..^𝑁) ∪ {𝑁})) |
112 | 107, 111 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
((0..^𝑁) ∪ {𝑁})) |
113 | 112 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
114 | 113 | raleqdv 3121 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
115 | 101, 114 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
116 | | ccatlen 13213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 ∈ Word 𝑉 ∧ 〈“𝑆”〉 ∈ Word 𝑉) → (#‘(𝑇 ++ 〈“𝑆”〉)) = ((#‘𝑇) + (#‘〈“𝑆”〉))) |
117 | 3, 18, 116 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (#‘(𝑇 ++ 〈“𝑆”〉)) = ((#‘𝑇) + (#‘〈“𝑆”〉))) |
118 | 117 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ((#‘(𝑇 ++ 〈“𝑆”〉)) − 1) =
(((#‘𝑇) +
(#‘〈“𝑆”〉)) − 1)) |
119 | | simpl2 1058 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (#‘𝑇) = (𝑁 + 1)) |
120 | | s1len 13238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(#‘〈“𝑆”〉) = 1 |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (#‘〈“𝑆”〉) =
1) |
122 | 119, 121 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ((#‘𝑇) + (#‘〈“𝑆”〉)) = ((𝑁 + 1) + 1)) |
123 | 122 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (((#‘𝑇) + (#‘〈“𝑆”〉)) − 1) = (((𝑁 + 1) + 1) −
1)) |
124 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
125 | 124 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
126 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 + 1) ∈ ℂ ∧ 1
∈ ℂ) → (((𝑁
+ 1) + 1) − 1) = (𝑁 +
1)) |
127 | 125, 60, 126 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
128 | 127 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1)) |
129 | 118, 123,
128 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ((#‘(𝑇 ++ 〈“𝑆”〉)) − 1) = (𝑁 + 1)) |
130 | 129 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) − 1)) = (0..^(𝑁 + 1))) |
131 | 130 | raleqdv 3121 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
132 | 115, 131 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
133 | 16, 20, 132 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → ((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
134 | 117, 122 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)) |
135 | 133, 134 | jca 553 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸))) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))) |
136 | 135 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Word 𝑉 ∧ (#‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
137 | 2, 136 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
138 | 137 | expd 451 |
. . . . . . . . . 10
⊢ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))))) |
139 | 138 | com12 32 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))))) |
140 | 139 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))))) |
141 | 140 | imp 444 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
142 | | iswwlkn 26212 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 1) ∈
ℕ0) → ((𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ ((𝑇 ++ 〈“𝑆”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
143 | 124, 142 | syl3an3 1353 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑇 ++
〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ ((𝑇 ++ 〈“𝑆”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
144 | | iswwlk 26211 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑇 ++ 〈“𝑆”〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
145 | 144 | anbi1d 737 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (((𝑇 ++ 〈“𝑆”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
146 | 145 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (((𝑇 ++
〈“𝑆”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
147 | 143, 146 | bitrd 267 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑇 ++
〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
148 | 147 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
149 | 141, 148 | sylibrd 248 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) |
150 | 149 | ex 449 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
151 | 150 | 3expa 1257 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
152 | 151 | adantrr 749 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑇 ∈ Word 𝑉)) → (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
153 | 1, 152 | mpcom 37 |
. 2
⊢ (𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) |
154 | 153 | 3impib 1254 |
1
⊢ ((𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) |