Step | Hyp | Ref
| Expression |
1 | | uzuzle23 11605 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
2 | 1 | anim2i 591 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘2))) |
3 | | av-extwwlkfab.c |
. . . . 5
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
4 | 3 | av-numclwwlkovg 41518 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
5 | 2, 4 | syl 17 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
6 | 5 | 3adant1 1072 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
7 | | 3simpb 1052 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝐺 ∈ USGraph
∧ 𝑁 ∈
(ℤ≥‘3))) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3))) |
9 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) |
10 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
11 | | av-extwwlkfablem2 41510 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺)) |
12 | 8, 9, 10, 11 | syl2an3an 1378 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺)) |
13 | | simpl 472 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘0) = 𝑋) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘0) = 𝑋) |
15 | 12, 14 | jca 553 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋)) |
16 | 1 | anim2i 591 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2))) |
17 | 16 | 3adant2 1073 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝐺 ∈ USGraph
∧ 𝑁 ∈
(ℤ≥‘2))) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2))) |
19 | | av-extwwlkfablem1 41508 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑤‘0))) |
20 | 18, 9, 10, 19 | syl2an3an 1378 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑤‘0))) |
21 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑋 = (𝑤‘0) → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
22 | 21 | eqcoms 2618 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
24 | 23 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
25 | 20, 24 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋)) |
26 | 10, 13 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 2)) = 𝑋) |
27 | 26 | adantl 481 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 2)) = 𝑋) |
28 | 15, 25, 27 | 3jca 1235 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)) |
29 | 28 | ex 449 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
30 | | simpl 472 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘0) = 𝑋) |
31 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘(𝑁 − 2)) = 𝑋) |
32 | 30 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑤‘0)) |
33 | 31, 32 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
34 | 30, 33 | jca 553 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
35 | 34 | ex 449 |
. . . . . . . 8
⊢ ((𝑤‘0) = 𝑋 → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
36 | 35 | a1d 25 |
. . . . . . 7
⊢ ((𝑤‘0) = 𝑋 → ((𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
((𝑁 − 2) ClWWalkSN
𝐺) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
38 | 37 | 3imp 1249 |
. . . . 5
⊢ ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
((𝑁 − 2) ClWWalkSN
𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
39 | 29, 38 | impbid1 214 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
40 | | av-extwwlkfab.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (Vtx‘𝐺) |
41 | 40 | clwwlknbp 41193 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁)) |
42 | | ige3m2fz 12236 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁)) |
43 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) = 𝑁 → (1...(#‘𝑤)) = (1...𝑁)) |
44 | 43 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (1...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (1...𝑁))) |
45 | 42, 44 | syl5ibr 235 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
47 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → 𝑤 ∈ Word 𝑉) |
48 | 46, 47 | jctild 564 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
49 | 41, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
50 | 49 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
51 | 50 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
52 | 51 | imp 444 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
53 | | swrd0fv0 13292 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
55 | 54 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (𝑤‘0) = ((𝑤 substr 〈0, (𝑁 −
2)〉)‘0)) |
56 | 55 | eqeq1d 2612 |
. . . . . 6
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → ((𝑤‘0) = 𝑋 ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
57 | 56 | anbi2d 736 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋))) |
58 | 57 | 3anbi1d 1395 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
59 | | uz3m2nn 11607 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
60 | 59 | anim2i 591 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ)) |
61 | 60 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ)) |
62 | | av-extwwlkfab.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
63 | 62 | av-numclwwlkovf 41511 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ) → (𝑋𝐹(𝑁 − 2)) = {𝑤 ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
64 | 63 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ↔ (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
65 | 61, 64 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ↔ (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
66 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑤 substr 〈0, (𝑁 − 2)〉) → (𝑢‘0) = ((𝑤 substr 〈0, (𝑁 −
2)〉)‘0)) |
67 | 66 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑢 = (𝑤 substr 〈0, (𝑁 − 2)〉) → ((𝑢‘0) = 𝑋 ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
68 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
69 | 68 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋)) |
70 | 69 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑤 ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} = {𝑢 ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∣ (𝑢‘0) = 𝑋} |
71 | 67, 70 | elrab2 3333 |
. . . . . . . 8
⊢ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
72 | 65, 71 | syl6bb 275 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋))) |
73 | 72 | 3anbi1d 1395 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
74 | 73 | bicomd 212 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑤 substr
〈0, (𝑁 −
2)〉) ∈ ((𝑁
− 2) ClWWalkSN 𝐺)
∧ ((𝑤 substr 〈0,
(𝑁 −
2)〉)‘0) = 𝑋)
∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
75 | 74 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
76 | 39, 58, 75 | 3bitrd 293 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
77 | 76 | rabbidva 3163 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
78 | 6, 77 | eqtrd 2644 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |