MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wwlkext2clwwlk Structured version   Unicode version

Theorem wwlkext2clwwlk 24479
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 24362 . . 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 12573 . . . . . . . . 9  |-  ( Z  e.  V  ->  <" Z ">  e. Word  V )
43adantr 465 . . . . . . . 8  |-  ( ( Z  e.  V  /\  N  e.  NN0 )  ->  <" Z ">  e. Word  V )
5 ccatcl 12554 . . . . . . . 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 24363 . . . . . . . . . . 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 11827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0..^ N )  <->  ( i  e. 
NN0  /\  N  e.  NN  /\  i  <  N
) )
13 simp1 996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  e.  NN0 )
14 peano2nn 10544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  NN )
15143ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  ( N  +  1 )  e.  NN )
16 nn0re 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  NN0  ->  i  e.  RR )
17163ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  e.  RR )
18 nnre 10539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  NN  ->  N  e.  RR )
19183ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  N  e.  RR )
20 peano2re 9748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
2118, 20syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  RR )
22213ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  ( N  +  1 )  e.  RR )
23 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  <  N )
2418ltp1d 10472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  NN  ->  N  <  ( N  +  1 ) )
25243ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  N  <  ( N  +  1 ) )
2617, 19, 22, 23, 25lttrd 9738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  N  e.  NN  /\  i  <  N )  ->  i  <  ( N  +  1 ) )
27 elfzo0 11827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ ( N  +  1 ) )  <->  ( i  e. 
NN0  /\  ( N  +  1 )  e.  NN  /\  i  < 
( N  +  1 ) ) )
2813, 15, 26, 27syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12556 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  i  e.  ( 0..^ ( # `  W ) ) )  ->  ( ( W concat  <" Z "> ) `  i )  =  ( W `  i ) )
3810, 11, 36, 37syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . . . . . . . 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 11858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12556 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . . . . . . . . . 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 2536 . . . . . . . . . . . . . . . . . . . . . . 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 2900 . . . . . . . . . . . . . . . . . . . . . 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 1193 . . . . . . . . . . . . . . . . . 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 6289 . . . . . . . . . . . . . . . . . . . . . . . . 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 10801 . . . . . . . . . . . . . . . . . . . . . . . . . 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 9979 . . . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  N  =  ( ( # `
 W )  - 
1 ) )
6564fveq2d 5868 . . . . . . . . . . . . . . . . . . . . . 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 10821 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4451 . . . . . . . . . . . . . . . . . . . . . . . . . 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 12398 . . . . . . . . . . . . . . . . . . . . . . . . 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 12563 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  W  =/=  (/) )  ->  ( ( W concat  <" Z "> ) `  ( (
# `  W )  -  1 ) )  =  ( lastS  `  W
) )
769, 66, 74, 75syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( W concat  <" Z "> ) `  (
( # `  W )  -  1 ) )  =  ( lastS  `  W
) )
7765, 76eqtr2d 2509 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( lastS  `  W )  =  ( ( W concat  <" Z "> ) `  N
) )
78 fveq2 5864 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  +  1 )  =  ( # `  W
)  ->  ( ( W concat  <" Z "> ) `  ( N  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( # `  W
) ) )
7978eqcoms 2479 . . . . . . . . . . . . . . . . . . . . . . 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 12596 . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  ->  Z  =  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) )
8477, 83preq12d 4114 . . . . . . . . . . . . . . . . . . . 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 1154 . . . . . . . . . . . . . . . . . . 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 2536 . . . . . . . . . . . . . . . . . 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 5864 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  N  ->  (
( W concat  <" Z "> ) `  i
)  =  ( ( W concat  <" Z "> ) `  N ) )
91 oveq1 6289 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  N  ->  (
i  +  1 )  =  ( N  + 
1 ) )
9291fveq2d 5868 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  N  ->  (
( W concat  <" Z "> ) `  (
i  +  1 ) )  =  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) )
9390, 92preq12d 4114 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  N  ->  { ( ( W concat  <" Z "> ) `  i
) ,  ( ( W concat  <" Z "> ) `  ( i  +  1 ) ) }  =  { ( ( W concat  <" Z "> ) `  N
) ,  ( ( W concat  <" Z "> ) `  ( N  +  1 ) ) } )
9493eleq1d 2536 . . . . . . . . . . . . . . . . . 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 4062 . . . . . . . . . . . . . . . . 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 3685 . . . . . . . . . . . . . . 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 11115 . . . . . . . . . . . . . . . . . . 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 11882 . . . . . . . . . . . . . . . 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 3064 . . . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . . 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 12585 . . . . . . . . . . . . . . . . . 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 6297 . . . . . . . . . . . . . . . 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 6289 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( # `  W )  +  1 )  =  ( ( N  + 
1 )  +  1 ) )
114113oveq1d 6297 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  W )  =  ( N  + 
1 )  ->  (
( ( # `  W
)  +  1 )  -  1 )  =  ( ( ( N  +  1 )  +  1 )  -  1 ) )
115 ax-1cn 9546 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  CC
116 addcl 9570 . . . . . . . . . . . . . . . . . . . . . . . 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 9927 . . . . . . . . . . . . . . . . . . . . . . 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 2530 . . . . . . . . . . . . . . . . . . . . 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 1018 . . . . . . . . . . . . . . . . 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 2508 . . . . . . . . . . . . . . 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 6298 . . . . . . . . . . . . . 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 3064 . . . . . . . . . . . . 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 24380 . . . . . . . . . . . . 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 12597 . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . 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 12562 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  0  < 
( # `  W ) )  ->  ( ( W concat  <" Z "> ) `  0 )  =  ( W ` 
0 ) )
149148eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e. Word  V  /\  <" Z ">  e. Word  V  /\  0  < 
( # `  W ) )  ->  ( W `  0 )  =  ( ( W concat  <" Z "> ) `  0
) )
150142, 143, 147, 149syl3anc 1228 . . . . . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . . 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 2536 . . . . . . . . 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 1176 . . . . 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 9614 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  +  1 )  =  ( N  +  ( 1  +  1 ) ) )
168 1p1e2 10645 . . . . . . . . . . . . . . 15  |-  ( 1  +  1 )  =  2
169168oveq2i 6293 . . . . . . . . . . . . . 14  |-  ( N  +  ( 1  +  1 ) )  =  ( N  +  2 )
170167, 169syl6eq 2524 . . . . . . . . . . . . 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 2528 . . . . . . . . . . 11  |-  ( ( ( W  e. Word  V  /\  ( # `  W
)  =  ( N  +  1 ) )  /\  ( Z  e.  V  /\  N  e. 
NN0 ) )  -> 
( ( # `  W
)  +  1 )  =  ( N  + 
2 ) )
173164, 172eqtrd 2508 . . . . . . . . . 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 10808 . . . . . . . . . . . . 13  |-  2  e.  NN0
181180a1i 11 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  2  e. 
NN0 )
182179, 181nn0addcld 10852 . . . . . . . . . . 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 975 . . . . . . . . 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 24445 . . . . . . . 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 24444 . . . . . . . . 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 920 . . . 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 1194 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 973    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2814   _Vcvv 3113    u. cun 3474   (/)c0 3785   {csn 4027   {cpr 4029   class class class wbr 4447   ran crn 5000   ` cfv 5586  (class class class)co 6282   CCcc 9486   RRcr 9487   0cc0 9488   1c1 9489    + caddc 9491    < clt 9624    - cmin 9801   NNcn 10532   2c2 10581   NN0cn0 10791   ZZ>=cuz 11078  ..^cfzo 11788   #chash 12369  Word cword 12496   lastS clsw 12497   concat cconcat 12498   <"cs1 12499   WWalksN cwwlkn 24354   ClWWalks cclwwlk 24424   ClWWalksN cclwwlkn 24425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-map 7419  df-pm 7420  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-card 8316  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-2 10590  df-n0 10792  df-z 10861  df-uz 11079  df-fz 11669  df-fzo 11789  df-hash 12370  df-word 12504  df-lsw 12505  df-concat 12506  df-s1 12507  df-wwlk 24355  df-wwlkn 24356  df-clwwlk 24427  df-clwwlkn 24428
This theorem is referenced by:  numclwwlk2lem1  24779
  Copyright terms: Public domain W3C validator