Metamath Proof Explorer

Theorem wwlksext2clwwlk

Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypotheses clwwlkext2edg.v 
|- V = ( Vtx ` G )
clwwlkext2edg.e 
|- E = ( Edg ` G )
Assertion wwlksext2clwwlk 
|- ( ( W e. ( N WWalksN G ) /\ Z e. V ) -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v 
 |-  V = ( Vtx ` G )
2 clwwlkext2edg.e 
 |-  E = ( Edg ` G )
3 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
4 1 wrdeqi 
 |-  Word V = Word ( Vtx ` G )
5 4 eleq2i 
 |-  ( W e. Word V <-> W e. Word ( Vtx ` G ) )
6 5 biimpri 
 |-  ( W e. Word ( Vtx ` G ) -> W e. Word V )
7 6 3ad2ant2 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. Word V )
8 7 ad2antlr 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> W e. Word V )
9 s1cl 
 |-  ( Z e. V -> <" Z "> e. Word V )
10 9 adantl 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> <" Z "> e. Word V )
11 ccatcl 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V ) -> ( W ++ <" Z "> ) e. Word V )
12 8 10 11 syl2anc 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( W ++ <" Z "> ) e. Word V )
13 12 adantr 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( W ++ <" Z "> ) e. Word V )
14 1 2 wwlknp 
 |-  ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
15 simplll 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> W e. Word V )
16 9 adantr 
 |-  ( ( Z e. V /\ N e. NN0 ) -> <" Z "> e. Word V )
17 16 ad2antlr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> <" Z "> e. Word V )
18 elfzo0 
 |-  ( i e. ( 0 ..^ N ) <-> ( i e. NN0 /\ N e. NN /\ i < N ) )
19 simp1 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i e. NN0 )
20 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
21 20 3ad2ant2 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> ( N + 1 ) e. NN )
22 nn0re 
 |-  ( i e. NN0 -> i e. RR )
23 22 3ad2ant1 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i e. RR )
24 nnre 
 |-  ( N e. NN -> N e. RR )
25 24 3ad2ant2 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> N e. RR )
26 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
27 24 26 syl 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
28 27 3ad2ant2 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> ( N + 1 ) e. RR )
29 simp3 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i < N )
30 24 ltp1d 
 |-  ( N e. NN -> N < ( N + 1 ) )
31 30 3ad2ant2 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> N < ( N + 1 ) )
32 23 25 28 29 31 lttrd 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i < ( N + 1 ) )
33 elfzo0 
 |-  ( i e. ( 0 ..^ ( N + 1 ) ) <-> ( i e. NN0 /\ ( N + 1 ) e. NN /\ i < ( N + 1 ) ) )
34 19 21 32 33 syl3anbrc 
 |-  ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i e. ( 0 ..^ ( N + 1 ) ) )
35 18 34 sylbi 
 |-  ( i e. ( 0 ..^ N ) -> i e. ( 0 ..^ ( N + 1 ) ) )
36 35 adantl 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( N + 1 ) ) )
37 oveq2 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( N + 1 ) ) )
38 37 adantl 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( N + 1 ) ) )
39 38 eleq2d 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
40 39 ad2antrr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
41 36 40 mpbird 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
42 ccatval1 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" Z "> ) ` i ) = ( W ` i ) )
43 15 17 41 42 syl3anc 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W ++ <" Z "> ) ` i ) = ( W ` i ) )
44 fzonn0p1p1 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) )
45 44 adantl 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) )
46 37 eleq2d 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) )
47 46 ad3antlr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) )
48 45 47 mpbird 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) )
49 ccatval1 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V /\ ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
50 15 17 48 49 syl3anc 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
51 43 50 preq12d 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
52 51 ex 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) )
53 52 expcom 
 |-  ( ( Z e. V /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) )
54 53 expcom 
 |-  ( N e. NN0 -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) )
55 54 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) )
56 55 imp 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) )
57 56 expdcom 
 |-  ( W e. Word V -> ( ( # ` W ) = ( N + 1 ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) )
58 57 3imp1 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ i e. ( 0 ..^ N ) ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
59 58 eleq1d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ i e. ( 0 ..^ N ) ) -> ( { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
60 59 ralbidva 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
61 60 biimprd 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) )
62 61 3exp 
 |-  ( W e. Word V -> ( ( # ` W ) = ( N + 1 ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) )
63 62 com34 
 |-  ( W e. Word V -> ( ( # ` W ) = ( N + 1 ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) )
64 63 3imp1 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
65 64 adantr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
66 simpll 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> W e. Word V )
67 9 ad2antrl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> <" Z "> e. Word V )
68 nn0p1gt0 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )
69 68 ad2antll 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> 0 < ( N + 1 ) )
70 breq2 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
71 70 ad2antlr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
72 69 71 mpbird 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> 0 < ( # ` W ) )
73 hashneq0 
 |-  ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
74 73 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
75 72 74 mpbid 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> W =/= (/) )
76 ccatval1lsw 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
77 66 67 75 76 syl3anc 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
78 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
79 78 ad2antlr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
80 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
81 80 ad2antll 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> N e. CC )
82 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
83 81 82 syl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( N + 1 ) - 1 ) = N )
84 79 83 eqtrd 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( # ` W ) - 1 ) = N )
85 84 fveq2d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( ( W ++ <" Z "> ) ` N ) )
86 77 85 eqtr3d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( lastS ` W ) = ( ( W ++ <" Z "> ) ` N ) )
87 ccatws1ls 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = Z )
88 87 ad2ant2r 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = Z )
89 fveq2 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) )
90 89 ad2antlr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) )
91 88 90 eqtr3d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> Z = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) )
92 86 91 preq12d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } )
93 92 expcom 
 |-  ( ( Z e. V /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) )
94 93 expcom 
 |-  ( N e. NN0 -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) )
95 94 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) )
96 95 imp 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) )
97 96 com12 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) )
98 97 3adant3 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) )
99 98 imp 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } )
100 99 eleq1d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( { ( lastS ` W ) , Z } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) )
101 100 biimpa 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E )
102 simprl1 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> N e. NN0 )
103 102 adantr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> N e. NN0 )
104 fveq2 
 |-  ( i = N -> ( ( W ++ <" Z "> ) ` i ) = ( ( W ++ <" Z "> ) ` N ) )
105 fvoveq1 
 |-  ( i = N -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) )
106 104 105 preq12d 
 |-  ( i = N -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } )
107 106 eleq1d 
 |-  ( i = N -> ( { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) )
108 107 ralsng 
 |-  ( N e. NN0 -> ( A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) )
109 103 108 syl 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) )
110 101 109 mpbird 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
111 ralunb 
 |-  ( A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> ( A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) )
112 65 110 111 sylanbrc 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
113 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
114 102 113 sylib 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> N e. ( ZZ>= ` 0 ) )
115 114 adantr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> N e. ( ZZ>= ` 0 ) )
116 fzosplitsn 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
117 115 116 syl 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
118 112 117 raleqtrrdv 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ ( N + 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
119 ccatws1len 
 |-  ( W e. Word V -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) )
120 119 3ad2ant1 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) )
121 120 ad2antrr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) )
122 121 oveq1d 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( ( # ` ( W ++ <" Z "> ) ) - 1 ) = ( ( ( # ` W ) + 1 ) - 1 ) )
123 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) + 1 ) = ( ( N + 1 ) + 1 ) )
124 123 oveq1d 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) )
125 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
126 80 125 addcld 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
127 126 125 pncand 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
128 127 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
129 128 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
130 124 129 sylan9eq 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( N + 1 ) )
131 130 3ad2antl2 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( N + 1 ) )
132 131 adantr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( N + 1 ) )
133 122 132 eqtrd 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( ( # ` ( W ++ <" Z "> ) ) - 1 ) = ( N + 1 ) )
134 133 oveq2d 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) = ( 0 ..^ ( N + 1 ) ) )
135 118 134 raleqtrrdv 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
136 135 exp42 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( { ( lastS ` W ) , Z } e. E -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) )
137 14 136 syl 
 |-  ( W e. ( N WWalksN G ) -> ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( { ( lastS ` W ) , Z } e. E -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) )
138 137 imp41 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
139 138 adantrr 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E )
140 lswccats1 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( lastS ` ( W ++ <" Z "> ) ) = Z )
141 8 140 sylancom 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( lastS ` ( W ++ <" Z "> ) ) = Z )
142 68 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 < ( N + 1 ) )
143 70 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
144 142 143 mpbird 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 < ( # ` W ) )
145 144 ad2antlr 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> 0 < ( # ` W ) )
146 ccatfv0 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V /\ 0 < ( # ` W ) ) -> ( ( W ++ <" Z "> ) ` 0 ) = ( W ` 0 ) )
147 8 10 145 146 syl3anc 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( ( W ++ <" Z "> ) ` 0 ) = ( W ` 0 ) )
148 141 147 preq12d 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } = { Z , ( W ` 0 ) } )
149 148 eleq1d 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E <-> { Z , ( W ` 0 ) } e. E ) )
150 149 biimprcd 
 |-  ( { Z , ( W ` 0 ) } e. E -> ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) )
151 150 adantl 
 |-  ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) )
152 151 impcom 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E )
153 13 139 152 3jca 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) )
154 ccatws1len 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) )
155 154 3ad2ant2 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) )
156 123 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) + 1 ) = ( ( N + 1 ) + 1 ) )
157 80 125 125 addassd 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
158 1p1e2 
 |-  ( 1 + 1 ) = 2
159 158 oveq2i 
 |-  ( N + ( 1 + 1 ) ) = ( N + 2 )
160 157 159 eqtrdi 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
161 160 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
162 155 156 161 3eqtrd 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) )
163 162 ad3antlr 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) )
164 2nn 
 |-  2 e. NN
165 nn0nnaddcl 
 |-  ( ( N e. NN0 /\ 2 e. NN ) -> ( N + 2 ) e. NN )
166 164 165 mpan2 
 |-  ( N e. NN0 -> ( N + 2 ) e. NN )
167 166 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( N + 2 ) e. NN )
168 1 2 isclwwlknx 
 |-  ( ( N + 2 ) e. NN -> ( ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) ) )
169 167 168 syl 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) ) )
170 169 ad3antlr 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) ) )
171 153 163 170 mpbir2and 
 |-  ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) )
172 171 exp31 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> ( Z e. V -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) )
173 3 172 mpdan 
 |-  ( W e. ( N WWalksN G ) -> ( Z e. V -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) )
174 173 imp 
 |-  ( ( W e. ( N WWalksN G ) /\ Z e. V ) -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) )