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