Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wwlkext2clwwlk Structured version   Unicode version

Theorem wwlkext2clwwlk 30465
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.)
Assertion
Ref Expression
wwlkext2clwwlk  |-  ( ( W  e.  ( ( V WWalksN  E ) `  N
)  /\  Z  e.  V  /\  N  e.  NN0 )  ->  ( ( { ( lastS  `  W ) ,  Z }  e.  ran  E  /\  { Z , 
( W `  0
) }  e.  ran  E )  ->  ( W concat  <" Z "> )  e.  ( ( V ClWWalksN  E ) `  ( N  +  2 ) ) ) )

Proof of Theorem wwlkext2clwwlk
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 wwlknprop 30320 . . 3  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) ) )
2 simplrr 760 . . . . . . . 8  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  ->  W  e. Word  V )
3 s1cl 12293 . . . . . . . . 9  |-  ( Z  e.  V  ->  <" Z ">  e. Word  V )
43adantr 465 . . . . . . . 8  |-  ( ( Z  e.  V  /\  N  e.  NN0 )  ->  <" Z ">  e. Word  V )
5 ccatcl 12274 . . . . . . . 8  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V )  ->  ( W concat  <" Z "> )  e. Word  V )
62, 4, 5syl2an 477 . . . . . . 7  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( W concat  <" Z "> )  e. Word  V
)
76adantr 465 . . . . . 6  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  ( W concat  <" Z "> )  e. Word  V )
8 wwlknimp 30321 . . . . . . . . . . 11  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( W  e. Word  V  /\  ( # `  W )  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E
) )
9 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  W  e. Word  V )
109adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  ->  W  e. Word  V )
114ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  ->  <" Z ">  e. Word  V )
12 elfzo0 11587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0..^ N )  <->  ( i  e. 
NN0  /\  N  e.  NN  /\  i  <  N
) )
13 simp1 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  e.  NN0 )
14 peano2nn 10334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  NN )
15143ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  ( N  +  1 )  e.  NN )
16 nn0re 10588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  NN0  ->  i  e.  RR )
17163ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  e.  RR )
18 nnre 10329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  NN  ->  N  e.  RR )
19183ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  N  e.  RR )
20 peano2re 9542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
2118, 20syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  RR )
22213ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  ( N  +  1 )  e.  RR )
23 simp3 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  <  N )
2418ltp1d 10263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  NN  ->  N  <  ( N  +  1 ) )
25243ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  N  <  ( N  +  1 ) )
2617, 19, 22, 23, 25lttrd 9532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  <  ( N  +  1 ) )
27 elfzo0 11587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ ( N  +  1 ) )  <->  ( i  e. 
NN0  /\  ( N  +  1 )  e.  NN  /\  i  < 
( N  +  1 ) ) )
2813, 15, 26, 27syl3anbrc 1172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  e.  ( 0..^ ( N  +  1 ) ) )
2912, 28sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ N )  ->  i  e.  ( 0..^ ( N  + 
1 ) ) )
3029adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
i  e.  ( 0..^ ( N  +  1 ) ) )
31 oveq2 6099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
0..^ ( # `  W
) )  =  ( 0..^ ( N  + 
1 ) ) )
3231adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( 0..^ ( # `  W ) )  =  ( 0..^ ( N  +  1 ) ) )
3332eleq2d 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( i  e.  ( 0..^ ( # `  W
) )  <->  i  e.  ( 0..^ ( N  + 
1 ) ) ) )
3433adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( i  e.  ( 0..^ ( # `  W
) )  <->  i  e.  ( 0..^ ( N  + 
1 ) ) ) )
3534adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 ) ) ) )
3630, 35mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
i  e.  ( 0..^ ( # `  W
) ) )
37 ccatval1 12276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  i  e.  ( 0..^ ( # `  W ) ) )  ->  ( ( W concat  <" Z "> ) `  i )  =  ( W `  i ) )
3810, 11, 36, 37syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( ( W concat  <" Z "> ) `  i
)  =  ( W `
 i ) )
3938eqcomd 2448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( W `  i
)  =  ( ( W concat  <" Z "> ) `  i ) )
40 fzonn0p1p1 30216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ N )  ->  ( i  +  1 )  e.  ( 0..^ ( N  +  1 ) ) )
4140adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( i  +  1 )  e.  ( 0..^ ( N  +  1 ) ) )
4231eleq2d 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( i  +  1 )  e.  ( 0..^ ( # `  W
) )  <->  ( i  +  1 )  e.  ( 0..^ ( N  +  1 ) ) ) )
4342ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 ) ) ) )
4441, 43mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( i  +  1 )  e.  ( 0..^ ( # `  W
) ) )
45 ccatval1 12276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  ( i  +  1 )  e.  ( 0..^ ( # `  W ) ) )  ->  ( ( W concat  <" Z "> ) `  ( i  +  1 ) )  =  ( W `  ( i  +  1 ) ) )
4610, 11, 44, 45syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( ( W concat  <" Z "> ) `  (
i  +  1 ) )  =  ( W `
 ( i  +  1 ) ) )
4746eqcomd 2448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( W `  (
i  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) )
4839, 47preq12d 3962 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  ->  { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  =  { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) } )
4948eleq1d 2509 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  i  e.  ( 0..^ N ) )  -> 
( { ( W `
 i ) ,  ( W `  (
i  +  1 ) ) }  e.  ran  E  <->  { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
5049ralbidva 2731 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
5150biimpd 207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
5251ex 434 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( ( Z  e.  V  /\  N  e. 
NN0 )  ->  ( A. i  e.  (
0..^ N ) { ( W `  i
) ,  ( W `
 ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  (
0..^ N ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) ) )
5352com23 78 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E  ->  ( ( Z  e.  V  /\  N  e. 
NN0 )  ->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) ) )
54533impia 1184 . . . . . . . . . . . . . . . . . 18  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
5554com12 31 . . . . . . . . . . . . . . . . 17  |-  ( ( Z  e.  V  /\  N  e.  NN0 )  -> 
( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  ->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
5655adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E )  -> 
( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  ->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
5756impcom 430 . . . . . . . . . . . . . . 15  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
)
58 oveq1 6098 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( # `  W )  -  1 )  =  ( ( N  + 
1 )  -  1 ) )
5958ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( # `  W
)  -  1 )  =  ( ( N  +  1 )  - 
1 ) )
60 nn0cn 10589 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  NN0  ->  N  e.  CC )
6160ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  N  e.  CC )
62 pncan1 9772 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  CC  ->  (
( N  +  1 )  -  1 )  =  N )
6361, 62syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( N  + 
1 )  -  1 )  =  N )
6459, 63eqtr2d 2476 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  N  =  ( ( # `
 W )  - 
1 ) )
6564fveq2d 5695 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( W concat  <" Z "> ) `  N
)  =  ( ( W concat  <" Z "> ) `  ( (
# `  W )  -  1 ) ) )
664adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  <" Z ">  e. Word  V )
67 nn0p1gt0 10609 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  NN0  ->  0  < 
( N  +  1 ) )
6867ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
0  <  ( N  +  1 ) )
69 breq2 4296 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
0  <  ( # `  W
)  <->  0  <  ( N  +  1 ) ) )
7069ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( 0  <  ( # `
 W )  <->  0  <  ( N  +  1 ) ) )
7168, 70mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
0  <  ( # `  W
) )
72 hashneq0 12132 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( W  e. Word  V  ->  (
0  <  ( # `  W
)  <->  W  =/=  (/) ) )
739, 72syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( 0  <  ( # `
 W )  <->  W  =/=  (/) ) )
7471, 73mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  W  =/=  (/) )
75 ccatval1lsw 12283 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  W  =/=  (/) )  ->  ( ( W concat  <" Z "> ) `  ( (
# `  W )  -  1 ) )  =  ( lastS  `  W
) )
769, 66, 74, 75syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( W concat  <" Z "> ) `  (
( # `  W )  -  1 ) )  =  ( lastS  `  W
) )
7765, 76eqtr2d 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( lastS  `  W )  =  ( ( W concat  <" Z "> ) `  N
) )
78 fveq2 5691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  +  1 )  =  ( # `  W
)  ->  ( ( W concat  <" Z "> ) `  ( N  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( # `  W
) ) )
7978eqcoms 2446 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( W concat  <" Z "> ) `  ( N  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( # `  W ) ) )
8079ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( W concat  <" Z "> ) `  ( N  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( # `  W ) ) )
81 ccatws1ls 12311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  e. Word  V  /\  Z  e.  V )  ->  ( ( W concat  <" Z "> ) `  ( # `
 W ) )  =  Z )
8281ad2ant2r 746 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( W concat  <" Z "> ) `  ( # `
 W ) )  =  Z )
8380, 82eqtr2d 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  Z  =  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) )
8477, 83preq12d 3962 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  { ( lastS  `  W ) ,  Z }  =  { ( ( W concat  <" Z "> ) `  N ) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) } )
85843adantl3 1146 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  { ( lastS  `  W
) ,  Z }  =  { ( ( W concat  <" Z "> ) `  N ) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) } )
8685eleq1d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( { ( lastS  `  W ) ,  Z }  e.  ran  E  <->  { (
( W concat  <" Z "> ) `  N
) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) }  e.  ran  E
) )
8786biimpd 207 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( { ( lastS  `  W ) ,  Z }  e.  ran  E  ->  { ( ( W concat  <" Z "> ) `  N ) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) }  e.  ran  E
) )
8887impr 619 . . . . . . . . . . . . . . . 16  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  { ( ( W concat  <" Z "> ) `  N ) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) }  e.  ran  E
)
89 simprlr 762 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  N  e.  NN0 )
90 fveq2 5691 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  N  ->  (
( W concat  <" Z "> ) `  i
)  =  ( ( W concat  <" Z "> ) `  N ) )
91 oveq1 6098 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  N  ->  (
i  +  1 )  =  ( N  + 
1 ) )
9291fveq2d 5695 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  N  ->  (
( W concat  <" Z "> ) `  (
i  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) )
9390, 92preq12d 3962 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  N  ->  { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  =  { ( ( W concat  <" Z "> ) `  N
) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) } )
9493eleq1d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  N  ->  ( { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( ( W concat  <" Z "> ) `  N
) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) }  e.  ran  E
) )
9594ralsng 3912 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( A. i  e.  { N }  { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( ( W concat  <" Z "> ) `  N
) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) }  e.  ran  E
) )
9689, 95syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( A. i  e.  { N }  {
( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( ( W concat  <" Z "> ) `  N
) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) }  e.  ran  E
) )
9788, 96mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  A. i  e.  { N }  { (
( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
)
98 ralunb 3537 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( (
0..^ N )  u. 
{ N } ) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  <->  ( A. i  e.  ( 0..^ N ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  A. i  e.  { N }  { (
( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
9957, 97, 98sylanbrc 664 . . . . . . . . . . . . . 14  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  A. i  e.  ( ( 0..^ N )  u.  { N }
) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
)
100 elnn0uz 10898 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN0  <->  N  e.  ( ZZ>=
`  0 ) )
101100biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN0  ->  N  e.  ( ZZ>= `  0 )
)
102101ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E )  ->  N  e.  ( ZZ>= ` 
0 ) )
103102adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  N  e.  (
ZZ>= `  0 ) )
104 fzosplitsn 11633 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( 0..^ ( N  +  1 ) )  =  ( ( 0..^ N )  u.  { N }
) )
105103, 104syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( 0..^ ( N  +  1 ) )  =  ( ( 0..^ N )  u. 
{ N } ) )
106105raleqdv 2923 . . . . . . . . . . . . . 14  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( A. i  e.  ( 0..^ ( N  +  1 ) ) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( ( 0..^ N )  u. 
{ N } ) { ( ( W concat  <" Z "> ) `  i ) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
10799, 106mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  A. i  e.  ( 0..^ ( N  + 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
)
108 simp1 988 . . . . . . . . . . . . . . . . . 18  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  ->  W  e. Word  V )
109 simpll 753 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E )  ->  Z  e.  V )
110 ccatws1len 12304 . . . . . . . . . . . . . . . . . 18  |-  ( ( W  e. Word  V  /\  Z  e.  V )  ->  ( # `  ( W concat  <" Z "> ) )  =  ( ( # `  W
)  +  1 ) )
111108, 109, 110syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( # `  ( W concat  <" Z "> ) )  =  ( ( # `  W
)  +  1 ) )
112111oveq1d 6106 . . . . . . . . . . . . . . . 16  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( ( # `  ( W concat  <" Z "> ) )  - 
1 )  =  ( ( ( # `  W
)  +  1 )  -  1 ) )
113 oveq1 6098 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( # `  W )  +  1 )  =  ( ( N  + 
1 )  +  1 ) )
114113oveq1d 6106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( ( # `  W
)  +  1 )  -  1 )  =  ( ( ( N  +  1 )  +  1 )  -  1 ) )
115 ax-1cn 9340 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  CC
116 addcl 9364 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( N  +  1 )  e.  CC )
117 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  1  e.  CC )
118116, 117pncand 9720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( ( N  +  1 )  +  1 )  -  1 )  =  ( N  +  1 ) )
11960, 115, 118sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( ( ( N  +  1 )  +  1 )  -  1 )  =  ( N  +  1 ) )
120114, 119sylan9eqr 2497 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  NN0  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( ( ( # `  W )  +  1 )  -  1 )  =  ( N  + 
1 ) )
121120ex 434 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( ( # `  W
)  +  1 )  -  1 )  =  ( N  +  1 ) ) )
122121ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E )  -> 
( ( # `  W
)  =  ( N  +  1 )  -> 
( ( ( # `  W )  +  1 )  -  1 )  =  ( N  + 
1 ) ) )
123122com12 31 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( ( Z  e.  V  /\  N  e. 
NN0 )  /\  {
( lastS  `  W ) ,  Z }  e.  ran  E )  ->  ( (
( # `  W )  +  1 )  - 
1 )  =  ( N  +  1 ) ) )
1241233ad2ant2 1010 . . . . . . . . . . . . . . . . 17  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  ->  (
( ( Z  e.  V  /\  N  e. 
NN0 )  /\  {
( lastS  `  W ) ,  Z }  e.  ran  E )  ->  ( (
( # `  W )  +  1 )  - 
1 )  =  ( N  +  1 ) ) )
125124imp 429 . . . . . . . . . . . . . . . 16  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( ( (
# `  W )  +  1 )  - 
1 )  =  ( N  +  1 ) )
126112, 125eqtrd 2475 . . . . . . . . . . . . . . 15  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( ( # `  ( W concat  <" Z "> ) )  - 
1 )  =  ( N  +  1 ) )
127126oveq2d 6107 . . . . . . . . . . . . . 14  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  -  1 ) )  =  ( 0..^ ( N  + 
1 ) ) )
128127raleqdv 2923 . . . . . . . . . . . . 13  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  ( A. i  e.  ( 0..^ ( (
# `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( N  +  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
129107, 128mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  /\  (
( Z  e.  V  /\  N  e.  NN0 )  /\  { ( lastS  `  W
) ,  Z }  e.  ran  E ) )  ->  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
)
130129exp32 605 . . . . . . . . . . 11  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 )  /\  A. i  e.  ( 0..^ N ) { ( W `  i ) ,  ( W `  ( i  +  1 ) ) }  e.  ran  E )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  ( { ( lastS  `  W ) ,  Z }  e.  ran  E  ->  A. i  e.  (
0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) ) )
1318, 130syl 16 . . . . . . . . . 10  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( ( Z  e.  V  /\  N  e.  NN0 )  -> 
( { ( lastS  `  W
) ,  Z }  e.  ran  E  ->  A. i  e.  ( 0..^ ( (
# `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) ) )
132131adantl 466 . . . . . . . . 9  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  ( { ( lastS  `  W ) ,  Z }  e.  ran  E  ->  A. i  e.  (
0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) ) )
133132imp 429 . . . . . . . 8  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( { ( lastS  `  W ) ,  Z }  e.  ran  E  ->  A. i  e.  (
0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
134133adantrd 468 . . . . . . 7  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( ( { ( lastS  `  W ) ,  Z }  e.  ran  E  /\  { Z , 
( W `  0
) }  e.  ran  E )  ->  A. i  e.  ( 0..^ ( (
# `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
) )
135134imp 429 . . . . . 6  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  A. i  e.  ( 0..^ ( (
# `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E
)
136 wwlknimpb 30338 . . . . . . . . . . . . 13  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( W  e. Word  V  /\  ( # `  W )  =  ( N  +  1 ) ) )
137 simpll 753 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  ->  W  e. Word  V
)
138 simpl 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Z  e.  V  /\  N  e.  NN0 )  ->  Z  e.  V )
139 lswccats1 12312 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( W  e. Word  V  /\  Z  e.  V )  ->  ( lastS  `  ( W concat  <" Z "> ) )  =  Z )
140137, 138, 139syl2an 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( lastS  `  ( W concat  <" Z "> ) )  =  Z )
141140eqcomd 2448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  Z  =  ( lastS  `  ( W concat  <" Z "> ) ) )
142137adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  W  e. Word  V )
1434adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  <" Z ">  e. Word  V )
14467adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  ->  0  <  ( N  +  1 ) )
14569ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  ->  ( 0  < 
( # `  W )  <->  0  <  ( N  +  1 ) ) )
146144, 145mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  ->  0  <  ( # `
 W ) )
147146adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
0  <  ( # `  W
) )
148 ccatfv0 12282 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  0  < 
( # `  W ) )  ->  ( ( W concat  <" Z "> ) `  0 )  =  ( W ` 
0 ) )
149148eqcomd 2448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  0  < 
( # `  W ) )  ->  ( W `  0 )  =  ( ( W concat  <" Z "> ) `  0
) )
150142, 143, 147, 149syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( W `  0
)  =  ( ( W concat  <" Z "> ) `  0 ) )
151141, 150preq12d 3962 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  N  e.  NN0 )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  { Z ,  ( W `
 0 ) }  =  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } )
152151exp31 604 . . . . . . . . . . . . . . . 16  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( N  e.  NN0  ->  ( ( Z  e.  V  /\  N  e. 
NN0 )  ->  { Z ,  ( W ` 
0 ) }  =  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } ) ) )
153152com12 31 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( ( Z  e.  V  /\  N  e. 
NN0 )  ->  { Z ,  ( W ` 
0 ) }  =  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } ) ) )
154153adantr 465 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  W  e. Word  V )  ->  ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  ->  ( ( Z  e.  V  /\  N  e.  NN0 )  ->  { Z ,  ( W ` 
0 ) }  =  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } ) ) )
155154adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( ( W  e. Word  V  /\  ( # `
 W )  =  ( N  +  1 ) )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  { Z , 
( W `  0
) }  =  {
( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } ) ) )
156136, 155syl5com 30 . . . . . . . . . . . 12  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( (
( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( ( Z  e.  V  /\  N  e.  NN0 )  ->  { Z ,  ( W `
 0 ) }  =  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } ) ) )
157156impcom 430 . . . . . . . . . . 11  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  { Z , 
( W `  0
) }  =  {
( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } ) )
158157imp 429 . . . . . . . . . 10  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  { Z , 
( W `  0
) }  =  {
( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) } )
159158eleq1d 2509 . . . . . . . . 9  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( { Z ,  ( W ` 
0 ) }  e.  ran  E  <->  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E ) )
160159biimpcd 224 . . . . . . . 8  |-  ( { Z ,  ( W `
 0 ) }  e.  ran  E  -> 
( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E ) )
161160adantl 466 . . . . . . 7  |-  ( ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E )  ->  ( ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E ) )
162161impcom 430 . . . . . 6  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E )
1637, 135, 1623jca 1168 . . . . 5  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  ( ( W concat  <" Z "> )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E ) )
164110ad2ant2r 746 . . . . . . . . . . 11  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( # `  ( W concat  <" Z "> ) )  =  ( ( # `  W
)  +  1 ) )
165113adantl 466 . . . . . . . . . . . 12  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( ( # `  W
)  +  1 )  =  ( ( N  +  1 )  +  1 ) )
166115a1i 11 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  1  e.  CC )
16760, 166, 166addassd 9408 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  +  1 )  =  ( N  +  ( 1  +  1 ) ) )
168 1p1e2 10435 . . . . . . . . . . . . . . 15  |-  ( 1  +  1 )  =  2
169168oveq2i 6102 . . . . . . . . . . . . . 14  |-  ( N  +  ( 1  +  1 ) )  =  ( N  +  2 )
170167, 169syl6eq 2491 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  +  1 )  =  ( N  +  2 ) )
171170adantl 466 . . . . . . . . . . . 12  |-  ( ( Z  e.  V  /\  N  e.  NN0 )  -> 
( ( N  + 
1 )  +  1 )  =  ( N  +  2 ) )
172165, 171sylan9eq 2495 . . . . . . . . . . 11  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( # `  W
)  +  1 )  =  ( N  + 
2 ) )
173164, 172eqtrd 2475 . . . . . . . . . 10  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) )
174173ex 434 . . . . . . . . 9  |-  ( ( W  e. Word  V  /\  ( # `  W )  =  ( N  + 
1 ) )  -> 
( ( Z  e.  V  /\  N  e. 
NN0 )  ->  ( # `
 ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) )
175136, 174syl 16 . . . . . . . 8  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( ( Z  e.  V  /\  N  e.  NN0 )  -> 
( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) )
176175adantl 466 . . . . . . 7  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  ( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) )
177176imp 429 . . . . . 6  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  /\  ( Z  e.  V  /\  N  e.  NN0 ) )  ->  ( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) )
178177adantr 465 . . . . 5  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  ( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) )
179 id 22 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  N  e. 
NN0 )
180 2nn0 10596 . . . . . . . . . . . . 13  |-  2  e.  NN0
181180a1i 11 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  2  e. 
NN0 )
182179, 181nn0addcld 10640 . . . . . . . . . . 11  |-  ( N  e.  NN0  ->  ( N  +  2 )  e. 
NN0 )
183182adantr 465 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  W  e. Word  V )  ->  ( N  +  2 )  e.  NN0 )
184183anim2i 569 . . . . . . . . 9  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  +  2 )  e.  NN0 ) )
185 df-3an 967 . . . . . . . . 9  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  ( N  +  2 )  e.  NN0 )  <->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  +  2 )  e.  NN0 ) )
186184, 185sylibr 212 . . . . . . . 8  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( V  e.  _V  /\  E  e. 
_V  /\  ( N  +  2 )  e. 
NN0 ) )
187 isclwwlkn 30432 . . . . . . . 8  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  ( N  +  2 )  e.  NN0 )  -> 
( ( W concat  <" Z "> )  e.  ( ( V ClWWalksN  E ) `  ( N  +  2 ) )  <->  ( ( W concat  <" Z "> )  e.  ( V ClWWalks  E )  /\  ( # `
 ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) ) )
188186, 187syl 16 . . . . . . 7  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( ( W concat  <" Z "> )  e.  (
( V ClWWalksN  E ) `  ( N  +  2
) )  <->  ( ( W concat  <" Z "> )  e.  ( V ClWWalks  E )  /\  ( # `
 ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) ) )
189 isclwwlk 30431 . . . . . . . . 9  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( ( W concat  <" Z "> )  e.  ( V ClWWalks  E )  <->  ( ( W concat  <" Z "> )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E ) ) )
190189adantr 465 . . . . . . . 8  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( ( W concat  <" Z "> )  e.  ( V ClWWalks  E )  <->  ( ( W concat  <" Z "> )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  -  1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E ) ) )
191190anbi1d 704 . . . . . . 7  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( (
( W concat  <" Z "> )  e.  ( V ClWWalks  E )  /\  ( # `
 ( W concat  <" Z "> ) )  =  ( N  +  2 ) )  <->  ( (
( W concat  <" Z "> )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E )  /\  ( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) ) )
192188, 191bitrd 253 . . . . . 6  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  ->  ( ( W concat  <" Z "> )  e.  (
( V ClWWalksN  E ) `  ( N  +  2
) )  <->  ( (
( W concat  <" Z "> )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E )  /\  ( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) ) )
193192ad3antrrr 729 . . . . 5  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  ( ( W concat  <" Z "> )  e.  (
( V ClWWalksN  E ) `  ( N  +  2
) )  <->  ( (
( W concat  <" Z "> )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( W concat  <" Z "> ) )  - 
1 ) ) { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( W concat  <" Z "> ) ) ,  ( ( W concat  <" Z "> ) `  0
) }  e.  ran  E )  /\  ( # `  ( W concat  <" Z "> ) )  =  ( N  +  2 ) ) ) )
194163, 178, 193mpbir2and 913 . . . 4  |-  ( ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E
) `  N )
)  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  /\  ( { ( lastS  `  W
) ,  Z }  e.  ran  E  /\  { Z ,  ( W `  0 ) }  e.  ran  E ) )  ->  ( W concat  <" Z "> )  e.  ( ( V ClWWalksN  E ) `  ( N  +  2 ) ) )
195194exp31 604 . . 3  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( N  e.  NN0  /\  W  e. Word  V ) )  /\  W  e.  ( ( V WWalksN  E ) `  N
) )  ->  (
( Z  e.  V  /\  N  e.  NN0 )  ->  ( ( { ( lastS  `  W ) ,  Z }  e.  ran  E  /\  { Z , 
( W `  0
) }  e.  ran  E )  ->  ( W concat  <" Z "> )  e.  ( ( V ClWWalksN  E ) `  ( N  +  2 ) ) ) ) )
1961, 195mpancom 669 . 2  |-  ( W  e.  ( ( V WWalksN  E ) `  N
)  ->  ( ( Z  e.  V  /\  N  e.  NN0 )  -> 
( ( { ( lastS  `  W ) ,  Z }  e.  ran  E  /\  { Z ,  ( W `
 0 ) }  e.  ran  E )  ->  ( W concat  <" Z "> )  e.  ( ( V ClWWalksN  E ) `  ( N  +  2 ) ) ) ) )
1971963impib 1185 1  |-  ( ( W  e.  ( ( V WWalksN  E ) `  N
)  /\  Z  e.  V  /\  N  e.  NN0 )  ->  ( ( { ( lastS  `  W ) ,  Z }  e.  ran  E  /\  { Z , 
( W `  0
) }  e.  ran  E )  ->  ( W concat  <" Z "> )  e.  ( ( V ClWWalksN  E ) `  ( N  +  2 ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756    =/= wne 2606   A.wral 2715   _Vcvv 2972    u. cun 3326   (/)c0 3637   {csn 3877   {cpr 3879   class class class wbr 4292   ran crn 4841   ` cfv 5418  (class class class)co 6091   CCcc 9280   RRcr 9281   0cc0 9282   1c1 9283    + caddc 9285    < clt 9418    - cmin 9595   NNcn 10322   2c2 10371   NN0cn0 10579   ZZ>=cuz 10861  ..^cfzo 11548   #chash 12103  Word cword 12221   lastS clsw 12222   concat cconcat 12223   <"cs1 12224   WWalksN cwwlkn 30312   ClWWalks cclwwlk 30413   ClWWalksN cclwwlkn 30414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-1o 6920  df-oadd 6924  df-er 7101  df-map 7216  df-pm 7217  df-en 7311  df-dom 7312  df-sdom 7313  df-fin 7314  df-card 8109  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-nn 10323  df-2 10380  df-n0 10580  df-z 10647  df-uz 10862  df-fz 11438  df-fzo 11549  df-hash 12104  df-word 12229  df-lsw 12230  df-concat 12231  df-s1 12232  df-wwlk 30313  df-wwlkn 30314  df-clwwlk 30416  df-clwwlkn 30417
This theorem is referenced by:  numclwwlk2lem1  30695
  Copyright terms: Public domain W3C validator