Step | Hyp | Ref
| Expression |
1 | | uzuzle23 11729 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
2 | 1 | anim2i 593 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘2))) |
3 | | extwwlkfab.c |
. . . . 5
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
4 | 3 | numclwwlkovg 27220 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
5 | 2, 4 | syl 17 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
6 | 5 | 3adant1 1079 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
7 | | 3simpb 1059 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝐺 ∈ USGraph
∧ 𝑁 ∈
(ℤ≥‘3))) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3))) |
9 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) |
10 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
11 | | extwwlkfablem2 27210 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺)) |
12 | 8, 9, 10, 11 | syl2an3an 1386 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺)) |
13 | | simpl 473 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘0) = 𝑋) |
14 | 13 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘0) = 𝑋) |
15 | 12, 14 | jca 554 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋)) |
16 | 1 | anim2i 593 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2))) |
17 | 16 | 3adant2 1080 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝐺 ∈ USGraph
∧ 𝑁 ∈
(ℤ≥‘2))) |
18 | 17 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2))) |
19 | | extwwlkfablem1 27207 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑤‘0))) |
20 | 18, 9, 10, 19 | syl2an3an 1386 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑤‘0))) |
21 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑋 = (𝑤‘0) → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
22 | 21 | eqcoms 2630 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
23 | 22 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
24 | 23 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝐺 NeighbVtx 𝑋) = (𝐺 NeighbVtx (𝑤‘0))) |
25 | 20, 24 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋)) |
26 | 10, 13 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 2)) = 𝑋) |
27 | 26 | adantl 482 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 2)) = 𝑋) |
28 | 15, 25, 27 | 3jca 1242 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)) |
29 | 28 | ex 450 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
30 | | simpl 473 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘0) = 𝑋) |
31 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘(𝑁 − 2)) = 𝑋) |
32 | 30 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑤‘0)) |
33 | 31, 32 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
34 | 30, 33 | jca 554 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
35 | 34 | ex 450 |
. . . . . . . 8
⊢ ((𝑤‘0) = 𝑋 → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
36 | 35 | a1d 25 |
. . . . . . 7
⊢ ((𝑤‘0) = 𝑋 → ((𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
37 | 36 | adantl 482 |
. . . . . 6
⊢ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
((𝑁 − 2) ClWWalksN
𝐺) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) → ((𝑤‘(𝑁 − 2)) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
38 | 37 | 3imp 1256 |
. . . . 5
⊢ ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
((𝑁 − 2) ClWWalksN
𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
39 | 29, 38 | impbid1 215 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
40 | | ige3m2fz 12365 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁)) |
41 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 𝑁 → (1...(#‘𝑤)) = (1...𝑁)) |
42 | 41 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (1...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (1...𝑁))) |
43 | 40, 42 | syl5ibr 236 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
45 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → 𝑤 ∈ Word 𝑉) |
46 | 44, 45 | jctild 566 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
47 | | extwwlkfab.v |
. . . . . . . . . . . . 13
⊢ 𝑉 = (Vtx‘𝐺) |
48 | 47 | clwwlknbp 26885 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝑁 ClWWalksN 𝐺) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁)) |
49 | 46, 48 | syl11 33 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤 ∈ (𝑁 ClWWalksN 𝐺) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
50 | 49 | 3ad2ant3 1084 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ (𝑁 ClWWalksN 𝐺) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))))) |
51 | 50 | imp 445 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
52 | | swrd0fv0 13440 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
54 | 53 | eqcomd 2628 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑤‘0) = ((𝑤 substr 〈0, (𝑁 −
2)〉)‘0)) |
55 | 54 | eqeq1d 2624 |
. . . . . 6
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑤‘0) = 𝑋 ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
56 | 55 | anbi2d 740 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋))) |
57 | 56 | 3anbi1d 1403 |
. . . 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)) = 𝑋))) |
58 | | uz3m2nn 11731 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
59 | 58 | anim2i 593 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ)) |
60 | 59 | 3adant1 1079 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ)) |
61 | | extwwlkfab.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
62 | 61 | numclwwlkovf 27213 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ) → (𝑋𝐹(𝑁 − 2)) = {𝑤 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
63 | 62 | eleq2d 2687 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ↔ (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
64 | 60, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ↔ (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
65 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑤 substr 〈0, (𝑁 − 2)〉) → (𝑢‘0) = ((𝑤 substr 〈0, (𝑁 −
2)〉)‘0)) |
66 | 65 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑢 = (𝑤 substr 〈0, (𝑁 − 2)〉) → ((𝑢‘0) = 𝑋 ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
67 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
68 | 67 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋)) |
69 | 68 | cbvrabv 3199 |
. . . . . . . . 9
⊢ {𝑤 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} = {𝑢 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∣ (𝑢‘0) = 𝑋} |
70 | 66, 69 | elrab2 3366 |
. . . . . . . 8
⊢ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ {𝑤 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋)) |
71 | 64, 70 | syl6bb 276 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋))) |
72 | 71 | 3anbi1d 1403 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
73 | 72 | bicomd 213 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑤 substr
〈0, (𝑁 −
2)〉) ∈ ((𝑁
− 2) ClWWalksN 𝐺)
∧ ((𝑤 substr 〈0,
(𝑁 −
2)〉)‘0) = 𝑋)
∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
74 | 73 | adantr 481 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = 𝑋) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
75 | 39, 57, 74 | 3bitrd 294 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋))) |
76 | 75 | rabbidva 3188 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |
77 | 6, 76 | eqtrd 2656 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑋𝐹(𝑁 − 2)) ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)}) |