Step | Hyp | Ref
| Expression |
1 | | uzuzle23 11605 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
2 | | numclwwlk.c |
. . . . 5
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
3 | | numclwwlk.f |
. . . . 5
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
4 | | numclwwlk.g |
. . . . 5
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
5 | 2, 3, 4 | numclwwlkovg 26614 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐺𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
6 | 1, 5 | sylan2 490 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐺𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
7 | 6 | 3adant1 1072 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐺𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
8 | | eluzge2nn0 11603 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
9 | 2 | numclwwlkfvc 26604 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
10 | 1, 8, 9 | 3syl 18 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
11 | 10 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
12 | 11 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ (𝐶‘𝑁) ↔ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
13 | 2 | extwwlkfablem2 26605 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2))) |
14 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘0) = 𝑋) |
15 | 14 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘0) = 𝑋) |
16 | 13, 15 | jca 553 |
. . . . . . . . . . 11
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋)) |
17 | 1 | 3anim3i 1243 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘2))) |
18 | | extwwlkfablem1 26601 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
19 | 17, 18 | sylanl1 680 |
. . . . . . . . . . 11
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
20 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
21 | 20, 14 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 2)) = 𝑋) |
22 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 2)) = 𝑋) |
23 | 16, 19, 22 | 3jca 1235 |
. . . . . . . . . 10
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)) |
24 | 23 | ex 449 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
25 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘0) = 𝑋) |
26 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘(𝑁 − 2)) = 𝑋) |
27 | 25 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑤‘0)) |
28 | 26, 27 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
29 | 25, 28 | jca 553 |
. . . . . . . . . . . . 13
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
30 | 29 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑤‘0) = 𝑋 → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
31 | 30 | a1d 25 |
. . . . . . . . . . 11
⊢ ((𝑤‘0) = 𝑋 → ((𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
32 | 31 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
33 | 32 | 3imp 1249 |
. . . . . . . . 9
⊢ ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
34 | 24, 33 | impbid1 214 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
35 | | clwwlknimp 26304 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸)) |
36 | | ige3m2fz 12236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁)) |
37 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑤) = 𝑁 → (1...(#‘𝑤)) = (1...𝑁)) |
38 | 37 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (1...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (1...𝑁))) |
39 | 36, 38 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
41 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → 𝑤 ∈ Word 𝑉) |
42 | 40, 41 | jctild 564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
43 | 42 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
44 | 35, 43 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
45 | 44 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
46 | 45 | 3ad2ant3 1077 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
47 | 46 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
48 | | swrd0fv0 13292 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
50 | 49 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑤‘0) = ((𝑤 substr 〈0, (𝑁 −
2)〉)‘0)) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑤‘0) = 𝑋 ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
52 | 51 | anbi2d 736 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋))) |
53 | 52 | 3anbi1d 1395 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
54 | 34, 53 | bitrd 267 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
55 | 54 | ex 449 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)))) |
56 | 12, 55 | sylbid 229 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ (𝐶‘𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)))) |
57 | 56 | imp 444 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝐶‘𝑁)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
58 | | uznn0sub 11595 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
59 | 1, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
ℕ0) |
60 | 2, 3 | numclwwlkovf 26608 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ0)
→ (𝑋𝐹(𝑁 − 2)) = {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋}) |
61 | 59, 60 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐹(𝑁 − 2)) = {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋}) |
62 | 61 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐹(𝑁 − 2)) = {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋}) |
63 | 62 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝐶‘𝑁)) → (𝑋𝐹(𝑁 − 2)) = {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋}) |
64 | 63 | eleq2d 2673 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝐶‘𝑁)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ↔ (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋})) |
65 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑢 = (𝑤 substr 〈0, (𝑁 − 2)〉) → (𝑢‘0) = ((𝑤 substr 〈0, (𝑁 −
2)〉)‘0)) |
66 | 65 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑢 = (𝑤 substr 〈0, (𝑁 − 2)〉) → ((𝑢‘0) = 𝑋 ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
67 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
68 | 67 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋)) |
69 | 68 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋} = {𝑢 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑢‘0) = 𝑋} |
70 | 66, 69 | elrab2 3333 |
. . . . . 6
⊢ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ (𝐶‘(𝑁 − 2)) ∣ (𝑤‘0) = 𝑋} ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
71 | 64, 70 | syl6rbb 276 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝐶‘𝑁)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ↔ (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)))) |
72 | 71 | 3anbi1d 1395 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝐶‘𝑁)) → ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2)) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
73 | 57, 72 | bitrd 267 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝐶‘𝑁)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
74 | 73 | rabbidva 3163 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
75 | 7, 74 | eqtrd 2644 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐺𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |