Step | Hyp | Ref
| Expression |
1 | | uzuzle23 12821 |
. . . 4
β’ (π β
(β€β₯β3) β π β
(β€β₯β2)) |
2 | | extwwlkfab.c |
. . . . 5
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
3 | 2 | 2clwwlk 29333 |
. . . 4
β’ ((π β π β§ π β (β€β₯β2))
β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) |
4 | 1, 3 | sylan2 594 |
. . 3
β’ ((π β π β§ π β (β€β₯β3))
β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) |
5 | 4 | 3adant1 1131 |
. 2
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) |
6 | | clwwlknon 29076 |
. . . 4
β’ (π(ClWWalksNOnβπΊ)π) = {π€ β (π ClWWalksN πΊ) β£ (π€β0) = π} |
7 | 6 | rabeqi 3423 |
. . 3
β’ {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} = {π€ β {π€ β (π ClWWalksN πΊ) β£ (π€β0) = π} β£ (π€β(π β 2)) = π} |
8 | | rabrab 3433 |
. . . 4
β’ {π€ β {π€ β (π ClWWalksN πΊ) β£ (π€β0) = π} β£ (π€β(π β 2)) = π} = {π€ β (π ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β(π β 2)) = π)} |
9 | | simpll3 1215 |
. . . . . . . . . . 11
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β π β
(β€β₯β3)) |
10 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β π€ β (π ClWWalksN πΊ)) |
11 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π€β0) = π β§ (π€β(π β 2)) = π) β (π€β(π β 2)) = π) |
12 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ (((π€β0) = π β§ (π€β(π β 2)) = π) β (π€β0) = π) |
13 | 12 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (((π€β0) = π β§ (π€β(π β 2)) = π) β π = (π€β0)) |
14 | 11, 13 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π€β0) = π β§ (π€β(π β 2)) = π) β (π€β(π β 2)) = (π€β0)) |
15 | 14 | adantl 483 |
. . . . . . . . . . 11
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (π€β(π β 2)) = (π€β0)) |
16 | | clwwnrepclwwn 29330 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β3) β§ π€ β (π ClWWalksN πΊ) β§ (π€β(π β 2)) = (π€β0)) β (π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ)) |
17 | 9, 10, 15, 16 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ)) |
18 | 12 | adantl 483 |
. . . . . . . . . 10
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (π€β0) = π) |
19 | 17, 18 | jca 513 |
. . . . . . . . 9
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β ((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π)) |
20 | | simp1 1137 |
. . . . . . . . . . . . 13
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β πΊ β
USGraph) |
21 | 20 | anim1i 616 |
. . . . . . . . . . . 12
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β (πΊ β USGraph β§ π€ β (π ClWWalksN πΊ))) |
22 | 21 | adantr 482 |
. . . . . . . . . . 11
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (πΊ β USGraph β§ π€ β (π ClWWalksN πΊ))) |
23 | | clwwlknlbonbgr1 29025 |
. . . . . . . . . . 11
β’ ((πΊ β USGraph β§ π€ β (π ClWWalksN πΊ)) β (π€β(π β 1)) β (πΊ NeighbVtx (π€β0))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (π€β(π β 1)) β (πΊ NeighbVtx (π€β0))) |
25 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π = (π€β0) β (πΊ NeighbVtx π) = (πΊ NeighbVtx (π€β0))) |
26 | 25 | eqcoms 2745 |
. . . . . . . . . . . 12
β’ ((π€β0) = π β (πΊ NeighbVtx π) = (πΊ NeighbVtx (π€β0))) |
27 | 26 | adantr 482 |
. . . . . . . . . . 11
β’ (((π€β0) = π β§ (π€β(π β 2)) = π) β (πΊ NeighbVtx π) = (πΊ NeighbVtx (π€β0))) |
28 | 27 | adantl 483 |
. . . . . . . . . 10
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (πΊ NeighbVtx π) = (πΊ NeighbVtx (π€β0))) |
29 | 24, 28 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (π€β(π β 1)) β (πΊ NeighbVtx π)) |
30 | 11 | adantl 483 |
. . . . . . . . 9
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (π€β(π β 2)) = π) |
31 | 19, 29, 30 | 3jca 1129 |
. . . . . . . 8
β’ ((((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β§ ((π€β0) = π β§ (π€β(π β 2)) = π)) β (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π)) |
32 | 31 | ex 414 |
. . . . . . 7
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β (((π€β0) = π β§ (π€β(π β 2)) = π) β (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
33 | | simpr 486 |
. . . . . . . . 9
β’ (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β (π€β0) = π) |
34 | 33 | anim1i 616 |
. . . . . . . 8
β’ ((((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β§ (π€β(π β 2)) = π) β ((π€β0) = π β§ (π€β(π β 2)) = π)) |
35 | 34 | 3adant2 1132 |
. . . . . . 7
β’ ((((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π) β ((π€β0) = π β§ (π€β(π β 2)) = π)) |
36 | 32, 35 | impbid1 224 |
. . . . . 6
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β (((π€β0) = π β§ (π€β(π β 2)) = π) β (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
37 | | 2clwwlklem 29329 |
. . . . . . . . . . . 12
β’ ((π€ β (π ClWWalksN πΊ) β§ π β (β€β₯β3))
β ((π€ prefix (π β 2))β0) = (π€β0)) |
38 | 37 | 3ad2antr3 1191 |
. . . . . . . . . . 11
β’ ((π€ β (π ClWWalksN πΊ) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β ((π€ prefix (π β 2))β0) = (π€β0)) |
39 | 38 | ancoms 460 |
. . . . . . . . . 10
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β ((π€ prefix (π β 2))β0) = (π€β0)) |
40 | 39 | eqcomd 2743 |
. . . . . . . . 9
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β (π€β0) = ((π€ prefix (π β 2))β0)) |
41 | 40 | eqeq1d 2739 |
. . . . . . . 8
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β ((π€β0) = π β ((π€ prefix (π β 2))β0) = π)) |
42 | 41 | anbi2d 630 |
. . . . . . 7
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β ((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π))) |
43 | 42 | 3anbi1d 1441 |
. . . . . 6
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β ((((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ (π€β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π) β (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
44 | | extwwlkfab.f |
. . . . . . . . . . 11
β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) |
45 | 44 | eleq2i 2830 |
. . . . . . . . . 10
β’ ((π€ prefix (π β 2)) β πΉ β (π€ prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2))) |
46 | | isclwwlknon 29077 |
. . . . . . . . . . 11
β’ ((π€ prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π)) |
47 | 46 | a1i 11 |
. . . . . . . . . 10
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π€ prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π))) |
48 | 45, 47 | bitrid 283 |
. . . . . . . . 9
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π€ prefix (π β 2)) β πΉ β ((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π))) |
49 | 48 | 3anbi1d 1441 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π) β (((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
50 | 49 | bicomd 222 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π) β ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
51 | 50 | adantr 482 |
. . . . . 6
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β ((((π€ prefix (π β 2)) β ((π β 2) ClWWalksN πΊ) β§ ((π€ prefix (π β 2))β0) = π) β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π) β ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
52 | 36, 43, 51 | 3bitrd 305 |
. . . . 5
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π€ β (π ClWWalksN πΊ)) β (((π€β0) = π β§ (π€β(π β 2)) = π) β ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π))) |
53 | 52 | rabbidva 3417 |
. . . 4
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β {π€ β (π ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β(π β 2)) = π)} = {π€ β (π ClWWalksN πΊ) β£ ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π)}) |
54 | 8, 53 | eqtrid 2789 |
. . 3
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β {π€ β {π€ β (π ClWWalksN πΊ) β£ (π€β0) = π} β£ (π€β(π β 2)) = π} = {π€ β (π ClWWalksN πΊ) β£ ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π)}) |
55 | 7, 54 | eqtrid 2789 |
. 2
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} = {π€ β (π ClWWalksN πΊ) β£ ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π)}) |
56 | 5, 55 | eqtrd 2777 |
1
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (ππΆπ) = {π€ β (π ClWWalksN πΊ) β£ ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π)}) |