This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwlkf

Description: Lemma 1 for clwwlkf1o : F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlkf1o.d 
|- D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
clwwlkf1o.f 
|- F = ( t e. D |-> ( t prefix N ) )
Assertion clwwlkf 
|- ( N e. NN -> F : D --> ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d 
 |-  D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
2 clwwlkf1o.f 
 |-  F = ( t e. D |-> ( t prefix N ) )
3 fveq2 
 |-  ( w = t -> ( lastS ` w ) = ( lastS ` t ) )
4 fveq1 
 |-  ( w = t -> ( w ` 0 ) = ( t ` 0 ) )
5 3 4 eqeq12d 
 |-  ( w = t -> ( ( lastS ` w ) = ( w ` 0 ) <-> ( lastS ` t ) = ( t ` 0 ) ) )
6 5 1 elrab2 
 |-  ( t e. D <-> ( t e. ( N WWalksN G ) /\ ( lastS ` t ) = ( t ` 0 ) ) )
7 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
8 iswwlksn 
 |-  ( N e. NN0 -> ( t e. ( N WWalksN G ) <-> ( t e. ( WWalks ` G ) /\ ( # ` t ) = ( N + 1 ) ) ) )
9 7 8 syl 
 |-  ( N e. NN -> ( t e. ( N WWalksN G ) <-> ( t e. ( WWalks ` G ) /\ ( # ` t ) = ( N + 1 ) ) ) )
10 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
11 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
12 10 11 iswwlks 
 |-  ( t e. ( WWalks ` G ) <-> ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
13 12 a1i 
 |-  ( N e. NN -> ( t e. ( WWalks ` G ) <-> ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
14 13 anbi1d 
 |-  ( N e. NN -> ( ( t e. ( WWalks ` G ) /\ ( # ` t ) = ( N + 1 ) ) <-> ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) )
15 9 14 bitrd 
 |-  ( N e. NN -> ( t e. ( N WWalksN G ) <-> ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) )
16 simpll 
 |-  ( ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) /\ N e. NN ) -> t e. Word ( Vtx ` G ) )
17 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
18 7 17 syl 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
19 nnre 
 |-  ( N e. NN -> N e. RR )
20 19 lep1d 
 |-  ( N e. NN -> N <_ ( N + 1 ) )
21 elfz2nn0 
 |-  ( N e. ( 0 ... ( N + 1 ) ) <-> ( N e. NN0 /\ ( N + 1 ) e. NN0 /\ N <_ ( N + 1 ) ) )
22 7 18 20 21 syl3anbrc 
 |-  ( N e. NN -> N e. ( 0 ... ( N + 1 ) ) )
23 22 adantl 
 |-  ( ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) /\ N e. NN ) -> N e. ( 0 ... ( N + 1 ) ) )
24 oveq2 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( 0 ... ( # ` t ) ) = ( 0 ... ( N + 1 ) ) )
25 24 eleq2d 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( N e. ( 0 ... ( # ` t ) ) <-> N e. ( 0 ... ( N + 1 ) ) ) )
26 25 adantl 
 |-  ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. ( 0 ... ( # ` t ) ) <-> N e. ( 0 ... ( N + 1 ) ) ) )
27 26 adantr 
 |-  ( ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) /\ N e. NN ) -> ( N e. ( 0 ... ( # ` t ) ) <-> N e. ( 0 ... ( N + 1 ) ) ) )
28 23 27 mpbird 
 |-  ( ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) /\ N e. NN ) -> N e. ( 0 ... ( # ` t ) ) )
29 16 28 jca 
 |-  ( ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) /\ N e. NN ) -> ( t e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` t ) ) ) )
30 pfxlen 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` t ) ) ) -> ( # ` ( t prefix N ) ) = N )
31 29 30 syl 
 |-  ( ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) /\ N e. NN ) -> ( # ` ( t prefix N ) ) = N )
32 31 ex 
 |-  ( ( t e. Word ( Vtx ` G ) /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. NN -> ( # ` ( t prefix N ) ) = N ) )
33 32 3ad2antl2 
 |-  ( ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. NN -> ( # ` ( t prefix N ) ) = N ) )
34 33 impcom 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( # ` ( t prefix N ) ) = N )
35 34 adantr 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( # ` ( t prefix N ) ) = N )
36 pfxcl 
 |-  ( t e. Word ( Vtx ` G ) -> ( t prefix N ) e. Word ( Vtx ` G ) )
37 36 3ad2ant2 
 |-  ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( t prefix N ) e. Word ( Vtx ` G ) )
38 37 ad2antrl 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( t prefix N ) e. Word ( Vtx ` G ) )
39 38 ad2antrl 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( t prefix N ) e. Word ( Vtx ` G ) )
40 oveq1 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( ( # ` t ) - 1 ) = ( ( N + 1 ) - 1 ) )
41 40 oveq2d 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( 0 ..^ ( ( # ` t ) - 1 ) ) = ( 0 ..^ ( ( N + 1 ) - 1 ) ) )
42 nncn 
 |-  ( N e. NN -> N e. CC )
43 1cnd 
 |-  ( N e. NN -> 1 e. CC )
44 42 43 pncand 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
45 44 oveq2d 
 |-  ( N e. NN -> ( 0 ..^ ( ( N + 1 ) - 1 ) ) = ( 0 ..^ N ) )
46 41 45 sylan9eqr 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( 0 ..^ ( ( # ` t ) - 1 ) ) = ( 0 ..^ N ) )
47 46 raleqdv 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
48 nnz 
 |-  ( N e. NN -> N e. ZZ )
49 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
50 48 49 syl 
 |-  ( N e. NN -> ( N - 1 ) e. ZZ )
51 19 lem1d 
 |-  ( N e. NN -> ( N - 1 ) <_ N )
52 eluz2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) <-> ( ( N - 1 ) e. ZZ /\ N e. ZZ /\ ( N - 1 ) <_ N ) )
53 50 48 51 52 syl3anbrc 
 |-  ( N e. NN -> N e. ( ZZ>= ` ( N - 1 ) ) )
54 fzoss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
55 53 54 syl 
 |-  ( N e. NN -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
56 55 adantr 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
57 ssralv 
 |-  ( ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) -> ( A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
58 56 57 syl 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
59 simplr 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> t e. Word ( Vtx ` G ) )
60 22 adantr 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> N e. ( 0 ... ( N + 1 ) ) )
61 25 adantl 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. ( 0 ... ( # ` t ) ) <-> N e. ( 0 ... ( N + 1 ) ) ) )
62 60 61 mpbird 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> N e. ( 0 ... ( # ` t ) ) )
63 62 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> N e. ( 0 ... ( # ` t ) ) )
64 55 sseld 
 |-  ( N e. NN -> ( i e. ( 0 ..^ ( N - 1 ) ) -> i e. ( 0 ..^ N ) ) )
65 64 ad2antrr 
 |-  ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) -> ( i e. ( 0 ..^ ( N - 1 ) ) -> i e. ( 0 ..^ N ) ) )
66 65 imp 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i e. ( 0 ..^ N ) )
67 pfxfv 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` t ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( t prefix N ) ` i ) = ( t ` i ) )
68 67 eqcomd 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` t ) ) /\ i e. ( 0 ..^ N ) ) -> ( t ` i ) = ( ( t prefix N ) ` i ) )
69 59 63 66 68 syl3anc 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( t ` i ) = ( ( t prefix N ) ` i ) )
70 48 ad2antrr 
 |-  ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) -> N e. ZZ )
71 elfzom1elp1fzo 
 |-  ( ( N e. ZZ /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ N ) )
72 70 71 sylan 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ N ) )
73 pfxfv 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` t ) ) /\ ( i + 1 ) e. ( 0 ..^ N ) ) -> ( ( t prefix N ) ` ( i + 1 ) ) = ( t ` ( i + 1 ) ) )
74 73 eqcomd 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` t ) ) /\ ( i + 1 ) e. ( 0 ..^ N ) ) -> ( t ` ( i + 1 ) ) = ( ( t prefix N ) ` ( i + 1 ) ) )
75 59 63 72 74 syl3anc 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( t ` ( i + 1 ) ) = ( ( t prefix N ) ` ( i + 1 ) ) )
76 69 75 preq12d 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> { ( t ` i ) , ( t ` ( i + 1 ) ) } = { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } )
77 76 eleq1d 
 |-  ( ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
78 77 ralbidva 
 |-  ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
79 78 biimpd 
 |-  ( ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) /\ t e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
80 79 ex 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( t e. Word ( Vtx ` G ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
81 80 com23 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( t e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
82 58 81 syld 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( t e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
83 47 82 sylbid 
 |-  ( ( N e. NN /\ ( # ` t ) = ( N + 1 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( t e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
84 83 ex 
 |-  ( N e. NN -> ( ( # ` t ) = ( N + 1 ) -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( t e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
85 84 com23 
 |-  ( N e. NN -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( # ` t ) = ( N + 1 ) -> ( t e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
86 85 com14 
 |-  ( t e. Word ( Vtx ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( # ` t ) = ( N + 1 ) -> ( N e. NN -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
87 86 imp 
 |-  ( ( t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( # ` t ) = ( N + 1 ) -> ( N e. NN -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
88 87 3adant1 
 |-  ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( # ` t ) = ( N + 1 ) -> ( N e. NN -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
89 88 imp 
 |-  ( ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. NN -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
90 89 impcom 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
91 90 ad2antrl 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
92 oveq1 
 |-  ( ( # ` ( t prefix N ) ) = N -> ( ( # ` ( t prefix N ) ) - 1 ) = ( N - 1 ) )
93 92 oveq2d 
 |-  ( ( # ` ( t prefix N ) ) = N -> ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) = ( 0 ..^ ( N - 1 ) ) )
94 93 adantr 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) = ( 0 ..^ ( N - 1 ) ) )
95 94 raleqdv 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
96 91 95 mpbird 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
97 simprl2 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> t e. Word ( Vtx ` G ) )
98 20 ancli 
 |-  ( N e. NN -> ( N e. NN /\ N <_ ( N + 1 ) ) )
99 48 peano2zd 
 |-  ( N e. NN -> ( N + 1 ) e. ZZ )
100 fznn 
 |-  ( ( N + 1 ) e. ZZ -> ( N e. ( 1 ... ( N + 1 ) ) <-> ( N e. NN /\ N <_ ( N + 1 ) ) ) )
101 99 100 syl 
 |-  ( N e. NN -> ( N e. ( 1 ... ( N + 1 ) ) <-> ( N e. NN /\ N <_ ( N + 1 ) ) ) )
102 98 101 mpbird 
 |-  ( N e. NN -> N e. ( 1 ... ( N + 1 ) ) )
103 102 adantr 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> N e. ( 1 ... ( N + 1 ) ) )
104 oveq2 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( 1 ... ( # ` t ) ) = ( 1 ... ( N + 1 ) ) )
105 104 eleq2d 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( N e. ( 1 ... ( # ` t ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
106 105 adantl 
 |-  ( ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. ( 1 ... ( # ` t ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
107 106 adantl 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( N e. ( 1 ... ( # ` t ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
108 103 107 mpbird 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> N e. ( 1 ... ( # ` t ) ) )
109 97 108 jca 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( t e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` t ) ) ) )
110 109 adantr 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( t e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` t ) ) ) )
111 pfxfvlsw 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` t ) ) ) -> ( lastS ` ( t prefix N ) ) = ( t ` ( N - 1 ) ) )
112 110 111 syl 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( lastS ` ( t prefix N ) ) = ( t ` ( N - 1 ) ) )
113 pfxfv0 
 |-  ( ( t e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` t ) ) ) -> ( ( t prefix N ) ` 0 ) = ( t ` 0 ) )
114 109 113 syl 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( ( t prefix N ) ` 0 ) = ( t ` 0 ) )
115 114 adantr 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( ( t prefix N ) ` 0 ) = ( t ` 0 ) )
116 112 115 preq12d 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } = { ( t ` ( N - 1 ) ) , ( t ` 0 ) } )
117 eqcom 
 |-  ( ( lastS ` t ) = ( t ` 0 ) <-> ( t ` 0 ) = ( lastS ` t ) )
118 117 biimpi 
 |-  ( ( lastS ` t ) = ( t ` 0 ) -> ( t ` 0 ) = ( lastS ` t ) )
119 118 adantl 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( t ` 0 ) = ( lastS ` t ) )
120 lsw 
 |-  ( t e. Word ( Vtx ` G ) -> ( lastS ` t ) = ( t ` ( ( # ` t ) - 1 ) ) )
121 120 3ad2ant2 
 |-  ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( lastS ` t ) = ( t ` ( ( # ` t ) - 1 ) ) )
122 121 ad2antrl 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( lastS ` t ) = ( t ` ( ( # ` t ) - 1 ) ) )
123 122 adantr 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( lastS ` t ) = ( t ` ( ( # ` t ) - 1 ) ) )
124 40 adantl 
 |-  ( ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) -> ( ( # ` t ) - 1 ) = ( ( N + 1 ) - 1 ) )
125 124 44 sylan9eqr 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> ( ( # ` t ) - 1 ) = N )
126 125 adantr 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( ( # ` t ) - 1 ) = N )
127 126 fveq2d 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( t ` ( ( # ` t ) - 1 ) ) = ( t ` N ) )
128 119 123 127 3eqtrd 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( t ` 0 ) = ( t ` N ) )
129 128 preq2d 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> { ( t ` ( N - 1 ) ) , ( t ` 0 ) } = { ( t ` ( N - 1 ) ) , ( t ` N ) } )
130 40 44 sylan9eq 
 |-  ( ( ( # ` t ) = ( N + 1 ) /\ N e. NN ) -> ( ( # ` t ) - 1 ) = N )
131 130 oveq2d 
 |-  ( ( ( # ` t ) = ( N + 1 ) /\ N e. NN ) -> ( 0 ..^ ( ( # ` t ) - 1 ) ) = ( 0 ..^ N ) )
132 131 raleqdv 
 |-  ( ( ( # ` t ) = ( N + 1 ) /\ N e. NN ) -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
133 fzo0end 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) )
134 fveq2 
 |-  ( i = ( N - 1 ) -> ( t ` i ) = ( t ` ( N - 1 ) ) )
135 fvoveq1 
 |-  ( i = ( N - 1 ) -> ( t ` ( i + 1 ) ) = ( t ` ( ( N - 1 ) + 1 ) ) )
136 134 135 preq12d 
 |-  ( i = ( N - 1 ) -> { ( t ` i ) , ( t ` ( i + 1 ) ) } = { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } )
137 136 eleq1d 
 |-  ( i = ( N - 1 ) -> ( { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
138 137 rspcva 
 |-  ( ( ( N - 1 ) e. ( 0 ..^ N ) /\ A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) )
139 133 138 sylan 
 |-  ( ( N e. NN /\ A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) )
140 42 43 npcand 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
141 140 fveq2d 
 |-  ( N e. NN -> ( t ` ( ( N - 1 ) + 1 ) ) = ( t ` N ) )
142 141 preq2d 
 |-  ( N e. NN -> { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } = { ( t ` ( N - 1 ) ) , ( t ` N ) } )
143 142 eleq1d 
 |-  ( N e. NN -> ( { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) <-> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
144 143 biimpd 
 |-  ( N e. NN -> ( { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
145 144 adantr 
 |-  ( ( N e. NN /\ A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( { ( t ` ( N - 1 ) ) , ( t ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
146 139 145 mpd 
 |-  ( ( N e. NN /\ A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) )
147 146 ex 
 |-  ( N e. NN -> ( A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
148 147 adantl 
 |-  ( ( ( # ` t ) = ( N + 1 ) /\ N e. NN ) -> ( A. i e. ( 0 ..^ N ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
149 132 148 sylbid 
 |-  ( ( ( # ` t ) = ( N + 1 ) /\ N e. NN ) -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
150 149 ex 
 |-  ( ( # ` t ) = ( N + 1 ) -> ( N e. NN -> ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) ) )
151 150 com3r 
 |-  ( A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( # ` t ) = ( N + 1 ) -> ( N e. NN -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) ) )
152 151 3ad2ant3 
 |-  ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( # ` t ) = ( N + 1 ) -> ( N e. NN -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) ) )
153 152 imp 
 |-  ( ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) -> ( N e. NN -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) ) )
154 153 impcom 
 |-  ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) )
155 154 adantr 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> { ( t ` ( N - 1 ) ) , ( t ` N ) } e. ( Edg ` G ) )
156 129 155 eqeltrd 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> { ( t ` ( N - 1 ) ) , ( t ` 0 ) } e. ( Edg ` G ) )
157 116 156 eqeltrd 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) )
158 157 adantl 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) )
159 39 96 158 3jca 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) )
160 simpl 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( # ` ( t prefix N ) ) = N )
161 159 160 jca 
 |-  ( ( ( # ` ( t prefix N ) ) = N /\ ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) )
162 35 161 mpancom 
 |-  ( ( ( N e. NN /\ ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) ) /\ ( lastS ` t ) = ( t ` 0 ) ) -> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) )
163 162 exp31 
 |-  ( N e. NN -> ( ( ( t =/= (/) /\ t e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` t ) - 1 ) ) { ( t ` i ) , ( t ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` t ) = ( N + 1 ) ) -> ( ( lastS ` t ) = ( t ` 0 ) -> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) ) ) )
164 15 163 sylbid 
 |-  ( N e. NN -> ( t e. ( N WWalksN G ) -> ( ( lastS ` t ) = ( t ` 0 ) -> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) ) ) )
165 164 imp32 
 |-  ( ( N e. NN /\ ( t e. ( N WWalksN G ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) )
166 10 11 isclwwlknx 
 |-  ( N e. NN -> ( ( t prefix N ) e. ( N ClWWalksN G ) <-> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) ) )
167 166 adantr 
 |-  ( ( N e. NN /\ ( t e. ( N WWalksN G ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( ( t prefix N ) e. ( N ClWWalksN G ) <-> ( ( ( t prefix N ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( t prefix N ) ) - 1 ) ) { ( ( t prefix N ) ` i ) , ( ( t prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( t prefix N ) ) , ( ( t prefix N ) ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` ( t prefix N ) ) = N ) ) )
168 165 167 mpbird 
 |-  ( ( N e. NN /\ ( t e. ( N WWalksN G ) /\ ( lastS ` t ) = ( t ` 0 ) ) ) -> ( t prefix N ) e. ( N ClWWalksN G ) )
169 6 168 sylan2b 
 |-  ( ( N e. NN /\ t e. D ) -> ( t prefix N ) e. ( N ClWWalksN G ) )
170 169 2 fmptd 
 |-  ( N e. NN -> F : D --> ( N ClWWalksN G ) )