Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝐺 ∈ USGraph
) |
2 | | uz3m2nn 11731 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
3 | 2 | 3ad2ant3 1084 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ) |
4 | | simp2 1062 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
5 | | extwwlkfab.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
6 | | extwwlkfab.v |
. . . . . . . . . . 11
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
8 | 5, 6, 7 | numclwwlkovfel2 27216 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧
𝑋 ∈ 𝑉) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋))) |
9 | 1, 3, 4, 8 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋))) |
10 | 5, 6, 7 | numclwwlkovf2ex 27219 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺)) |
11 | 10 | ad4ant134 1296 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺)) |
12 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) |
13 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋 ∈ 𝑉) |
14 | 6 | nbgrisvtx 26255 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑌 ∈ 𝑉) |
15 | 14 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑌 ∈ 𝑉) |
16 | 13, 15 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) |
17 | 16 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
18 | 17 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
20 | 19 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) |
21 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑁 ∈
(ℤ≥‘3)) |
22 | 12, 20, 21 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈
(ℤ≥‘3))) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈
(ℤ≥‘3))) |
24 | | numclwlk1lem2foalem 27222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) =
𝑊 ∧ (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) =
𝑊 ∧ (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)) |
26 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) =
𝑊 → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉) substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)))) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) =
𝑊 → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉) substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)))) |
28 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
31 | | idd 24 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋 → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)) |
32 | 27, 30, 31 | 3anim123d 1406 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → (((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) =
𝑊 ∧ (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))) |
33 | 25, 32 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)) |
34 | 11, 33 | jca 554 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))) |
35 | 34 | exp31 630 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2))) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))))) |
36 | 35 | expcom 451 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))))) |
37 | 36 | 3ad2antl1 1223 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = (𝑁 − 2)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))))) |
38 | 37 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))))) |
39 | 38 | com12 32 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))))) |
40 | 9, 39 | sylbid 230 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))))) |
41 | 40 | com14 96 |
. . . . . . 7
⊢ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))))) |
42 | 41 | pm2.43i 52 |
. . . . . 6
⊢ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))))) |
43 | 42 | imp 445 |
. . . . 5
⊢ ((𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)))) |
44 | 43 | impcom 446 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋))) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))) |
45 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → (𝑤 substr 〈0, (𝑁 − 2)〉) = (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉) substr 〈0, (𝑁 −
2)〉)) |
46 | 45 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ↔ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)))) |
47 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → (𝑤‘(𝑁 − 1)) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1))) |
48 | 47 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → ((𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ↔ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋))) |
49 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → (𝑤‘(𝑁 − 2)) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2))) |
50 | 49 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → ((𝑤‘(𝑁 − 2)) = 𝑋 ↔ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)) |
51 | 46, 48, 50 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑤 = ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))) |
52 | 51 | elrab 3363 |
. . . 4
⊢ (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉) ∈ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)} ↔ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ∧ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋))) |
53 | 44, 52 | sylibr 224 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
54 | | extwwlkfab.c |
. . . . 5
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
55 | 6, 5, 54 | extwwlkfab 27223 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
56 | 55 | adantr 481 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋))) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
57 | 53, 56 | eleqtrrd 2704 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑋𝐶𝑁)) |
58 | 57 | ex 450 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑋𝐶𝑁))) |