Metamath Proof Explorer

Theorem wwlksm1edg

Description: Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Assertion wwlksm1edg 
|- ( ( W e. ( WWalks ` G ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 iswwlks 
 |-  ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
4 lencl 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` W ) e. NN0 )
5 simpl 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. NN0 )
6 1red 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 1 e. RR )
7 2re 
 |-  2 e. RR
8 7 a1i 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 2 e. RR )
9 nn0re 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. RR )
10 9 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. RR )
11 1le2 
 |-  1 <_ 2
12 11 a1i 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 1 <_ 2 )
13 simpr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) )
14 6 8 10 12 13 letrd 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 1 <_ ( # ` W ) )
15 5 14 jca 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) e. NN0 /\ 1 <_ ( # ` W ) ) )
16 elnnnn0c 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ 1 <_ ( # ` W ) ) )
17 15 16 sylibr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. NN )
18 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
19 17 18 sylibr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
20 nn0ge2m1nn 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. NN )
21 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) <-> ( ( # ` W ) - 1 ) e. NN )
22 20 21 sylibr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
23 19 22 jca 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( 0 e. ( 0 ..^ ( # ` W ) ) /\ 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) )
24 4 23 sylan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( 0 e. ( 0 ..^ ( # ` W ) ) /\ 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) )
25 inelcm 
 |-  ( ( 0 e. ( 0 ..^ ( # ` W ) ) /\ 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( 0 ..^ ( # ` W ) ) i^i ( 0 ..^ ( ( # ` W ) - 1 ) ) ) =/= (/) )
26 24 25 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( 0 ..^ ( # ` W ) ) i^i ( 0 ..^ ( ( # ` W ) - 1 ) ) ) =/= (/) )
27 wrdfn 
 |-  ( W e. Word ( Vtx ` G ) -> W Fn ( 0 ..^ ( # ` W ) ) )
28 27 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> W Fn ( 0 ..^ ( # ` W ) ) )
29 fnresdisj 
 |-  ( W Fn ( 0 ..^ ( # ` W ) ) -> ( ( ( 0 ..^ ( # ` W ) ) i^i ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) <-> ( W |` ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) ) )
30 28 29 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( ( 0 ..^ ( # ` W ) ) i^i ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) <-> ( W |` ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) ) )
31 nn0ge2m1nn0 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
32 10 lem1d 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) <_ ( # ` W ) )
33 31 5 32 3jca 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) )
34 4 33 sylan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) )
35 elfz2nn0 
 |-  ( ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) <-> ( ( ( # ` W ) - 1 ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) )
36 34 35 sylibr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
37 pfxres 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) = ( W |` ( 0 ..^ ( ( # ` W ) - 1 ) ) ) )
38 37 eqeq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) = (/) <-> ( W |` ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) ) )
39 38 bicomd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W |` ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) <-> ( W prefix ( ( # ` W ) - 1 ) ) = (/) ) )
40 36 39 syldan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( W |` ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) <-> ( W prefix ( ( # ` W ) - 1 ) ) = (/) ) )
41 30 40 bitr2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) = (/) <-> ( ( 0 ..^ ( # ` W ) ) i^i ( 0 ..^ ( ( # ` W ) - 1 ) ) ) = (/) ) )
42 41 necon3bid 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) =/= (/) <-> ( ( 0 ..^ ( # ` W ) ) i^i ( 0 ..^ ( ( # ` W ) - 1 ) ) ) =/= (/) ) )
43 26 42 mpbird 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) =/= (/) )
44 43 3ad2antl2 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) =/= (/) )
45 pfxcl 
 |-  ( W e. Word ( Vtx ` G ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. Word ( Vtx ` G ) )
46 45 a1d 
 |-  ( W e. Word ( Vtx ` G ) -> ( 2 <_ ( # ` W ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. Word ( Vtx ` G ) ) )
47 46 3ad2ant2 
 |-  ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) -> ( 2 <_ ( # ` W ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. Word ( Vtx ` G ) ) )
48 47 imp 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. Word ( Vtx ` G ) )
49 nn0z 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
50 peano2zm 
 |-  ( ( # ` W ) e. ZZ -> ( ( # ` W ) - 1 ) e. ZZ )
51 49 50 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) e. ZZ )
52 peano2zm 
 |-  ( ( ( # ` W ) - 1 ) e. ZZ -> ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ )
53 51 52 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ )
54 53 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ )
55 51 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ZZ )
56 peano2rem 
 |-  ( ( # ` W ) e. RR -> ( ( # ` W ) - 1 ) e. RR )
57 9 56 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) e. RR )
58 57 lem1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) )
59 58 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) )
60 54 55 59 3jca 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ /\ ( ( # ` W ) - 1 ) e. ZZ /\ ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) ) )
61 4 60 sylan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ /\ ( ( # ` W ) - 1 ) e. ZZ /\ ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) ) )
62 eluz2 
 |-  ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( ( ( # ` W ) - 1 ) - 1 ) ) <-> ( ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ /\ ( ( # ` W ) - 1 ) e. ZZ /\ ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) ) )
63 61 62 sylibr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( ( ( # ` W ) - 1 ) - 1 ) ) )
64 9 lem1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) <_ ( # ` W ) )
65 64 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) <_ ( # ` W ) )
66 31 5 65 3jca 
 |-  ( ( ( # ` W ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) )
67 4 66 sylan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) )
68 67 35 sylibr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
69 pfxlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( ( # ` W ) - 1 ) )
70 69 oveq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) = ( ( ( # ` W ) - 1 ) - 1 ) )
71 68 70 syldan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) = ( ( ( # ` W ) - 1 ) - 1 ) )
72 71 fveq2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ZZ>= ` ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) = ( ZZ>= ` ( ( ( # ` W ) - 1 ) - 1 ) ) )
73 63 72 eleqtrrd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) )
74 fzoss2 
 |-  ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) -> ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
75 73 74 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
76 ssralv 
 |-  ( ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) -> ( A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
77 75 76 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
78 68 69 syldan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( ( # ` W ) - 1 ) )
79 78 oveq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) = ( ( ( # ` W ) - 1 ) - 1 ) )
80 79 oveq2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) = ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) )
81 80 eleq2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) <-> x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) )
82 simpl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> W e. Word ( Vtx ` G ) )
83 82 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> W e. Word ( Vtx ` G ) )
84 36 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
85 4 31 sylan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
86 nn0z 
 |-  ( ( ( # ` W ) - 1 ) e. NN0 -> ( ( # ` W ) - 1 ) e. ZZ )
87 fzossrbm1 
 |-  ( ( ( # ` W ) - 1 ) e. ZZ -> ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
88 86 87 syl 
 |-  ( ( ( # ` W ) - 1 ) e. NN0 -> ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
89 85 88 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) C_ ( 0 ..^ ( ( # ` W ) - 1 ) ) )
90 89 sselda 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
91 pfxfv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) = ( W ` x ) )
92 83 84 90 91 syl3anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) = ( W ` x ) )
93 92 eqcomd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( W ` x ) = ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) )
94 4 20 sylan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. NN )
95 elfzom1p1elfzo 
 |-  ( ( ( ( # ` W ) - 1 ) e. NN /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( x + 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
96 94 95 sylan 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( x + 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
97 pfxfv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) /\ ( x + 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) = ( W ` ( x + 1 ) ) )
98 83 84 96 97 syl3anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) = ( W ` ( x + 1 ) ) )
99 98 eqcomd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> ( W ` ( x + 1 ) ) = ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) )
100 93 99 preq12d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) ) -> { ( W ` x ) , ( W ` ( x + 1 ) ) } = { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } )
101 100 ex 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( x e. ( 0 ..^ ( ( ( # ` W ) - 1 ) - 1 ) ) -> { ( W ` x ) , ( W ` ( x + 1 ) ) } = { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } ) )
102 81 101 sylbid 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) -> { ( W ` x ) , ( W ` ( x + 1 ) ) } = { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } ) )
103 102 imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) ) -> { ( W ` x ) , ( W ` ( x + 1 ) ) } = { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } )
104 103 eleq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) ) -> ( { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) <-> { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
105 104 biimpd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) /\ x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) ) -> ( { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
106 105 ralimdva 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
107 77 106 syld 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 2 <_ ( # ` W ) ) -> ( A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
108 107 expcom 
 |-  ( 2 <_ ( # ` W ) -> ( W e. Word ( Vtx ` G ) -> ( A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) ) )
109 108 com3l 
 |-  ( W e. Word ( Vtx ` G ) -> ( A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( 2 <_ ( # ` W ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) ) )
110 109 a1i 
 |-  ( W =/= (/) -> ( W e. Word ( Vtx ` G ) -> ( A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( 2 <_ ( # ` W ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) ) ) )
111 110 3imp1 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) /\ 2 <_ ( # ` W ) ) -> A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) )
112 1 2 iswwlks 
 |-  ( ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) <-> ( ( W prefix ( ( # ` W ) - 1 ) ) =/= (/) /\ ( W prefix ( ( # ` W ) - 1 ) ) e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) { ( ( W prefix ( ( # ` W ) - 1 ) ) ` x ) , ( ( W prefix ( ( # ` W ) - 1 ) ) ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
113 44 48 111 112 syl3anbrc 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) )
114 113 ex 
 |-  ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` x ) , ( W ` ( x + 1 ) ) } e. ( Edg ` G ) ) -> ( 2 <_ ( # ` W ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) ) )
115 3 114 sylbi 
 |-  ( W e. ( WWalks ` G ) -> ( 2 <_ ( # ` W ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) ) )
116 115 imp 
 |-  ( ( W e. ( WWalks ` G ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) )