Metamath Proof Explorer

Theorem wwlksubclwwlk

Description: Any prefix of a word representing a closed walk represents a walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 28-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion wwlksubclwwlk 
|- ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( X e. ( N ClWWalksN G ) -> ( X prefix M ) e. ( ( M - 1 ) WWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 clwwlknp 
 |-  ( X e. ( N ClWWalksN G ) -> ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` X ) , ( X ` 0 ) } e. ( Edg ` G ) ) )
4 pfxcl 
 |-  ( X e. Word ( Vtx ` G ) -> ( X prefix M ) e. Word ( Vtx ` G ) )
5 4 adantr 
 |-  ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) -> ( X prefix M ) e. Word ( Vtx ` G ) )
6 5 ad2antrr 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( X prefix M ) e. Word ( Vtx ` G ) )
7 nnz 
 |-  ( M e. NN -> M e. ZZ )
8 eluzp1m1 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
9 8 ex 
 |-  ( M e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) ) )
10 7 9 syl 
 |-  ( M e. NN -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) ) )
11 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
12 7 11 syl 
 |-  ( M e. NN -> ( M - 1 ) e. ZZ )
13 nnre 
 |-  ( M e. NN -> M e. RR )
14 13 lem1d 
 |-  ( M e. NN -> ( M - 1 ) <_ M )
15 eluzuzle 
 |-  ( ( ( M - 1 ) e. ZZ /\ ( M - 1 ) <_ M ) -> ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) ) )
16 12 14 15 syl2anc 
 |-  ( M e. NN -> ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) ) )
17 10 16 syld 
 |-  ( M e. NN -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) ) )
18 17 imp 
 |-  ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
19 fzoss2 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) -> ( 0 ..^ ( M - 1 ) ) C_ ( 0 ..^ ( N - 1 ) ) )
20 18 19 syl 
 |-  ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( 0 ..^ ( M - 1 ) ) C_ ( 0 ..^ ( N - 1 ) ) )
21 20 adantl 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( 0 ..^ ( M - 1 ) ) C_ ( 0 ..^ ( N - 1 ) ) )
22 ssralv 
 |-  ( ( 0 ..^ ( M - 1 ) ) C_ ( 0 ..^ ( N - 1 ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( M - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
23 21 22 syl 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( M - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
24 simpll 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> X e. Word ( Vtx ` G ) )
25 24 adantr 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> X e. Word ( Vtx ` G ) )
26 eluz2 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ ( M + 1 ) <_ N ) )
27 13 adantr 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> M e. RR )
28 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
29 13 28 syl 
 |-  ( M e. NN -> ( M + 1 ) e. RR )
30 29 adantr 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> ( M + 1 ) e. RR )
31 zre 
 |-  ( N e. ZZ -> N e. RR )
32 31 ad2antrl 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> N e. RR )
33 13 lep1d 
 |-  ( M e. NN -> M <_ ( M + 1 ) )
34 33 adantr 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> M <_ ( M + 1 ) )
35 simpr 
 |-  ( ( N e. ZZ /\ ( M + 1 ) <_ N ) -> ( M + 1 ) <_ N )
36 35 adantl 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> ( M + 1 ) <_ N )
37 27 30 32 34 36 letrd 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> M <_ N )
38 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
39 38 ad2antrr 
 |-  ( ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) /\ M <_ N ) -> M e. NN0 )
40 simpr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> N e. ZZ )
41 40 adantr 
 |-  ( ( ( M e. NN /\ N e. ZZ ) /\ M <_ N ) -> N e. ZZ )
42 0red 
 |-  ( ( M e. NN /\ N e. ZZ ) -> 0 e. RR )
43 13 adantr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> M e. RR )
44 31 adantl 
 |-  ( ( M e. NN /\ N e. ZZ ) -> N e. RR )
45 42 43 44 3jca 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( 0 e. RR /\ M e. RR /\ N e. RR ) )
46 45 adantr 
 |-  ( ( ( M e. NN /\ N e. ZZ ) /\ M <_ N ) -> ( 0 e. RR /\ M e. RR /\ N e. RR ) )
47 38 nn0ge0d 
 |-  ( M e. NN -> 0 <_ M )
48 47 adantr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> 0 <_ M )
49 48 anim1i 
 |-  ( ( ( M e. NN /\ N e. ZZ ) /\ M <_ N ) -> ( 0 <_ M /\ M <_ N ) )
50 letr 
 |-  ( ( 0 e. RR /\ M e. RR /\ N e. RR ) -> ( ( 0 <_ M /\ M <_ N ) -> 0 <_ N ) )
51 46 49 50 sylc 
 |-  ( ( ( M e. NN /\ N e. ZZ ) /\ M <_ N ) -> 0 <_ N )
52 elnn0z 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
53 41 51 52 sylanbrc 
 |-  ( ( ( M e. NN /\ N e. ZZ ) /\ M <_ N ) -> N e. NN0 )
54 53 adantlrr 
 |-  ( ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) /\ M <_ N ) -> N e. NN0 )
55 simpr 
 |-  ( ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) /\ M <_ N ) -> M <_ N )
56 39 54 55 3jca 
 |-  ( ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) /\ M <_ N ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
57 37 56 mpdan 
 |-  ( ( M e. NN /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
58 57 expcom 
 |-  ( ( N e. ZZ /\ ( M + 1 ) <_ N ) -> ( M e. NN -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
59 58 3adant1 
 |-  ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ ( M + 1 ) <_ N ) -> ( M e. NN -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
60 26 59 sylbi 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( M e. NN -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
61 60 impcom 
 |-  ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
62 elfz2nn0 
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
63 61 62 sylibr 
 |-  ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> M e. ( 0 ... N ) )
64 63 adantl 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> M e. ( 0 ... N ) )
65 oveq2 
 |-  ( ( # ` X ) = N -> ( 0 ... ( # ` X ) ) = ( 0 ... N ) )
66 65 eleq2d 
 |-  ( ( # ` X ) = N -> ( M e. ( 0 ... ( # ` X ) ) <-> M e. ( 0 ... N ) ) )
67 66 adantl 
 |-  ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) -> ( M e. ( 0 ... ( # ` X ) ) <-> M e. ( 0 ... N ) ) )
68 67 adantr 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( M e. ( 0 ... ( # ` X ) ) <-> M e. ( 0 ... N ) ) )
69 64 68 mpbird 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> M e. ( 0 ... ( # ` X ) ) )
70 69 adantr 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> M e. ( 0 ... ( # ` X ) ) )
71 eluz2 
 |-  ( M e. ( ZZ>= ` ( M - 1 ) ) <-> ( ( M - 1 ) e. ZZ /\ M e. ZZ /\ ( M - 1 ) <_ M ) )
72 12 7 14 71 syl3anbrc 
 |-  ( M e. NN -> M e. ( ZZ>= ` ( M - 1 ) ) )
73 fzoss2 
 |-  ( M e. ( ZZ>= ` ( M - 1 ) ) -> ( 0 ..^ ( M - 1 ) ) C_ ( 0 ..^ M ) )
74 72 73 syl 
 |-  ( M e. NN -> ( 0 ..^ ( M - 1 ) ) C_ ( 0 ..^ M ) )
75 74 sseld 
 |-  ( M e. NN -> ( i e. ( 0 ..^ ( M - 1 ) ) -> i e. ( 0 ..^ M ) ) )
76 75 ad2antrl 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( i e. ( 0 ..^ ( M - 1 ) ) -> i e. ( 0 ..^ M ) ) )
77 76 imp 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> i e. ( 0 ..^ M ) )
78 pfxfv 
 |-  ( ( X e. Word ( Vtx ` G ) /\ M e. ( 0 ... ( # ` X ) ) /\ i e. ( 0 ..^ M ) ) -> ( ( X prefix M ) ` i ) = ( X ` i ) )
79 25 70 77 78 syl3anc 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> ( ( X prefix M ) ` i ) = ( X ` i ) )
80 79 eqcomd 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> ( X ` i ) = ( ( X prefix M ) ` i ) )
81 fzonn0p1p1 
 |-  ( i e. ( 0 ..^ ( M - 1 ) ) -> ( i + 1 ) e. ( 0 ..^ ( ( M - 1 ) + 1 ) ) )
82 nncn 
 |-  ( M e. NN -> M e. CC )
83 npcan1 
 |-  ( M e. CC -> ( ( M - 1 ) + 1 ) = M )
84 82 83 syl 
 |-  ( M e. NN -> ( ( M - 1 ) + 1 ) = M )
85 84 oveq2d 
 |-  ( M e. NN -> ( 0 ..^ ( ( M - 1 ) + 1 ) ) = ( 0 ..^ M ) )
86 85 eleq2d 
 |-  ( M e. NN -> ( ( i + 1 ) e. ( 0 ..^ ( ( M - 1 ) + 1 ) ) <-> ( i + 1 ) e. ( 0 ..^ M ) ) )
87 81 86 syl5ib 
 |-  ( M e. NN -> ( i e. ( 0 ..^ ( M - 1 ) ) -> ( i + 1 ) e. ( 0 ..^ M ) ) )
88 87 ad2antrl 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( i e. ( 0 ..^ ( M - 1 ) ) -> ( i + 1 ) e. ( 0 ..^ M ) ) )
89 88 imp 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ M ) )
90 pfxfv 
 |-  ( ( X e. Word ( Vtx ` G ) /\ M e. ( 0 ... ( # ` X ) ) /\ ( i + 1 ) e. ( 0 ..^ M ) ) -> ( ( X prefix M ) ` ( i + 1 ) ) = ( X ` ( i + 1 ) ) )
91 25 70 89 90 syl3anc 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> ( ( X prefix M ) ` ( i + 1 ) ) = ( X ` ( i + 1 ) ) )
92 91 eqcomd 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> ( X ` ( i + 1 ) ) = ( ( X prefix M ) ` ( i + 1 ) ) )
93 80 92 preq12d 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> { ( X ` i ) , ( X ` ( i + 1 ) ) } = { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } )
94 93 eleq1d 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) /\ i e. ( 0 ..^ ( M - 1 ) ) ) -> ( { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
95 94 ralbidva 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( A. i e. ( 0 ..^ ( M - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( M - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
96 23 95 sylibd 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( M - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
97 96 impancom 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> A. i e. ( 0 ..^ ( M - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
98 97 imp 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> A. i e. ( 0 ..^ ( M - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
99 24 69 jca 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( X e. Word ( Vtx ` G ) /\ M e. ( 0 ... ( # ` X ) ) ) )
100 99 adantlr 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( X e. Word ( Vtx ` G ) /\ M e. ( 0 ... ( # ` X ) ) ) )
101 pfxlen 
 |-  ( ( X e. Word ( Vtx ` G ) /\ M e. ( 0 ... ( # ` X ) ) ) -> ( # ` ( X prefix M ) ) = M )
102 100 101 syl 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( # ` ( X prefix M ) ) = M )
103 102 oveq1d 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( ( # ` ( X prefix M ) ) - 1 ) = ( M - 1 ) )
104 103 oveq2d 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) = ( 0 ..^ ( M - 1 ) ) )
105 104 raleqdv 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( M - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
106 98 105 mpbird 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
107 24 69 101 syl2anc 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( # ` ( X prefix M ) ) = M )
108 84 eqcomd 
 |-  ( M e. NN -> M = ( ( M - 1 ) + 1 ) )
109 108 ad2antrl 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> M = ( ( M - 1 ) + 1 ) )
110 107 109 eqtrd 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) )
111 110 adantlr 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) )
112 6 106 111 3jca 
 |-  ( ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) ) -> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) )
113 112 ex 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) ) )
114 113 3adant3 
 |-  ( ( ( X e. Word ( Vtx ` G ) /\ ( # ` X ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( X ` i ) , ( X ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` X ) , ( X ` 0 ) } e. ( Edg ` G ) ) -> ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) ) )
115 3 114 syl 
 |-  ( X e. ( N ClWWalksN G ) -> ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) ) )
116 115 impcom 
 |-  ( ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ X e. ( N ClWWalksN G ) ) -> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) )
117 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
118 117 ad2antrr 
 |-  ( ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ X e. ( N ClWWalksN G ) ) -> ( M - 1 ) e. NN0 )
119 1 2 iswwlksnx 
 |-  ( ( M - 1 ) e. NN0 -> ( ( X prefix M ) e. ( ( M - 1 ) WWalksN G ) <-> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) ) )
120 118 119 syl 
 |-  ( ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ X e. ( N ClWWalksN G ) ) -> ( ( X prefix M ) e. ( ( M - 1 ) WWalksN G ) <-> ( ( X prefix M ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( X prefix M ) ) - 1 ) ) { ( ( X prefix M ) ` i ) , ( ( X prefix M ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` ( X prefix M ) ) = ( ( M - 1 ) + 1 ) ) ) )
121 116 120 mpbird 
 |-  ( ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ X e. ( N ClWWalksN G ) ) -> ( X prefix M ) e. ( ( M - 1 ) WWalksN G ) )
122 121 ex 
 |-  ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( X e. ( N ClWWalksN G ) -> ( X prefix M ) e. ( ( M - 1 ) WWalksN G ) ) )