Metamath Proof Explorer

Theorem wwlksnred

Description: Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Assertion wwlksnred 
|- ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
2 iswwlksn 
 |-  ( ( N + 1 ) e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
6 4 5 iswwlks 
 |-  ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
7 simp1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> W e. Word ( Vtx ` G ) )
8 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
9 8 3ad2ant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) e. NN )
10 1 nn0red 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
11 10 lep1d 
 |-  ( N e. NN0 -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
12 11 3ad2ant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
13 breq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) <_ ( # ` W ) <-> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
14 13 3ad2ant2 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( ( N + 1 ) <_ ( # ` W ) <-> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
15 12 14 mpbird 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) <_ ( # ` W ) )
16 pfxn0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. NN /\ ( N + 1 ) <_ ( # ` W ) ) -> ( W prefix ( N + 1 ) ) =/= (/) )
17 7 9 15 16 syl3anc 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) =/= (/) )
18 17 3exp 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) =/= (/) ) ) )
19 18 3ad2ant2 
 |-  ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) =/= (/) ) ) )
20 19 imp 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) =/= (/) ) )
21 20 impcom 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( W prefix ( N + 1 ) ) =/= (/) )
22 pfxcl 
 |-  ( W e. Word ( Vtx ` G ) -> ( W prefix ( N + 1 ) ) e. Word ( Vtx ` G ) )
23 22 3ad2ant2 
 |-  ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( W prefix ( N + 1 ) ) e. Word ( Vtx ` G ) )
24 23 adantr 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( W prefix ( N + 1 ) ) e. Word ( Vtx ` G ) )
25 24 adantl 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( W prefix ( N + 1 ) ) e. Word ( Vtx ` G ) )
26 oveq1 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( # ` W ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) )
27 1 nn0cnd 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
28 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
29 27 28 pncand 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
30 26 29 sylan9eq 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( ( # ` W ) - 1 ) = ( N + 1 ) )
31 30 oveq2d 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = ( 0 ..^ ( N + 1 ) ) )
32 31 raleqdv 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
33 32 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
34 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
35 nn0z 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. ZZ )
36 1 35 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. ZZ )
37 nn0re 
 |-  ( N e. NN0 -> N e. RR )
38 37 lep1d 
 |-  ( N e. NN0 -> N <_ ( N + 1 ) )
39 34 36 38 3jca 
 |-  ( N e. NN0 -> ( N e. ZZ /\ ( N + 1 ) e. ZZ /\ N <_ ( N + 1 ) ) )
40 39 ad2antll 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( N e. ZZ /\ ( N + 1 ) e. ZZ /\ N <_ ( N + 1 ) ) )
41 eluz2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( N + 1 ) e. ZZ /\ N <_ ( N + 1 ) ) )
42 40 41 sylibr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
43 fzoss2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
44 42 43 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
45 ssralv 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
46 44 45 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
47 simpll 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> W e. Word ( Vtx ` G ) )
48 nn0fz0 
 |-  ( ( N + 1 ) e. NN0 <-> ( N + 1 ) e. ( 0 ... ( N + 1 ) ) )
49 1 48 sylib 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 0 ... ( N + 1 ) ) )
50 49 ad2antll 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( N + 1 ) e. ( 0 ... ( N + 1 ) ) )
51 fzelp1 
 |-  ( ( N + 1 ) e. ( 0 ... ( N + 1 ) ) -> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) )
52 50 51 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) )
53 oveq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( 0 ... ( # ` W ) ) = ( 0 ... ( ( N + 1 ) + 1 ) ) )
54 53 eleq2d 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) e. ( 0 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) ) )
55 54 adantr 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( ( N + 1 ) e. ( 0 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) ) )
56 55 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( ( N + 1 ) e. ( 0 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) ) )
57 52 56 mpbird 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( N + 1 ) e. ( 0 ... ( # ` W ) ) )
58 57 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( N + 1 ) e. ( 0 ... ( # ` W ) ) )
59 fzossfzop1 
 |-  ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
60 59 sseld 
 |-  ( N e. NN0 -> ( i e. ( 0 ..^ N ) -> i e. ( 0 ..^ ( N + 1 ) ) ) )
61 60 ad2antll 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( i e. ( 0 ..^ N ) -> i e. ( 0 ..^ ( N + 1 ) ) ) )
62 61 imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( N + 1 ) ) )
63 pfxfv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) /\ i e. ( 0 ..^ ( N + 1 ) ) ) -> ( ( W prefix ( N + 1 ) ) ` i ) = ( W ` i ) )
64 47 58 62 63 syl3anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W prefix ( N + 1 ) ) ` i ) = ( W ` i ) )
65 64 eqcomd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( W ` i ) = ( ( W prefix ( N + 1 ) ) ` i ) )
66 fzofzp1 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... N ) )
67 66 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ... N ) )
68 fzval3 
 |-  ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
69 68 eqcomd 
 |-  ( N e. ZZ -> ( 0 ..^ ( N + 1 ) ) = ( 0 ... N ) )
70 34 69 syl 
 |-  ( N e. NN0 -> ( 0 ..^ ( N + 1 ) ) = ( 0 ... N ) )
71 70 eleq2d 
 |-  ( N e. NN0 -> ( ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
72 71 ad2antll 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
73 72 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
74 67 73 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) )
75 pfxfv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) /\ ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) -> ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
76 47 58 74 75 syl3anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
77 76 eqcomd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( W ` ( i + 1 ) ) = ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) )
78 65 77 preq12d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } )
79 78 eleq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
80 79 biimpd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
81 80 ralimdva 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ N ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
82 46 81 syld 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ N ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
83 33 82 sylbid 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ N ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
84 83 imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ N ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
85 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
86 85 28 pncand 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
87 86 oveq2d 
 |-  ( N e. NN0 -> ( 0 ..^ ( ( N + 1 ) - 1 ) ) = ( 0 ..^ N ) )
88 87 ad2antll 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( 0 ..^ ( ( N + 1 ) - 1 ) ) = ( 0 ..^ N ) )
89 88 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( 0 ..^ ( ( N + 1 ) - 1 ) ) = ( 0 ..^ N ) )
90 89 raleqdv 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ N ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
91 84 90 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
92 pfxlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) )
93 57 92 syldan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) )
94 93 oveq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) = ( ( N + 1 ) - 1 ) )
95 94 oveq2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) = ( 0 ..^ ( ( N + 1 ) - 1 ) ) )
96 95 raleqdv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
97 96 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
98 91 97 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
99 98 exp31 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
100 99 com23 
 |-  ( W e. Word ( Vtx ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
101 100 imp 
 |-  ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
102 101 3adant1 
 |-  ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
103 102 expdimp 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
104 103 impcom 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
105 4 5 iswwlks 
 |-  ( ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) <-> ( ( W prefix ( N + 1 ) ) =/= (/) /\ ( W prefix ( N + 1 ) ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( W prefix ( N + 1 ) ) ) - 1 ) ) { ( ( W prefix ( N + 1 ) ) ` i ) , ( ( W prefix ( N + 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
106 21 25 104 105 syl3anbrc 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) )
107 peano2nn0 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
108 1 107 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
109 elfz2nn0 
 |-  ( ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) <-> ( ( N + 1 ) e. NN0 /\ ( ( N + 1 ) + 1 ) e. NN0 /\ ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
110 1 108 11 109 syl3anbrc 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) )
111 110 adantl 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) )
112 111 55 mpbird 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 0 ... ( # ` W ) ) )
113 112 anim2i 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) )
114 113 exp32 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) ) )
115 114 3ad2ant2 
 |-  ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) ) )
116 115 imp 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) )
117 116 impcom 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) )
118 117 92 syl 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) )
119 iswwlksn 
 |-  ( N e. NN0 -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) /\ ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) ) ) )
120 119 adantr 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) /\ ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) ) ) )
121 106 118 120 mpbir2and 
 |-  ( ( N e. NN0 /\ ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) )
122 121 expcom 
 |-  ( ( ( W =/= (/) /\ W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )
123 6 122 sylanb 
 |-  ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )
124 123 com12 
 |-  ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )
125 3 124 sylbid 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )