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

Theorem numclwwlkovf2ex 30684
Description: Extending a closed walk starting at a fixed vertex by an additional edge (forth and back). (Contributed by AV, 22-Sep-2018.) (Proof shortened by AV, 23-Oct-2018.)
Hypotheses
Ref Expression
numclwwlk.c  |-  C  =  ( n  e.  NN0  |->  ( ( V ClWWalksN  E ) `
 n ) )
numclwwlk.f  |-  F  =  ( v  e.  V ,  n  e.  NN0  |->  { w  e.  ( C `  n )  |  ( w ` 
0 )  =  v } )
Assertion
Ref Expression
numclwwlkovf2ex  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  Q  e.  ( <. V ,  E >. Neighbors  X )  /\  P  e.  ( X F ( N  -  2 ) ) )  ->  ( ( P concat  <" X "> ) concat  <" Q "> )  e.  ( C `  N ) )
Distinct variable groups:    n, E    n, N    n, V    w, C    w, N    C, n, v, w    v, N    n, X, v, w    v, V   
w, E    w, V    w, F    w, P    w, Q
Allowed substitution hints:    P( v, n)    Q( v, n)    E( v)    F( v, n)

Proof of Theorem numclwwlkovf2ex
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 simp1 988 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  V USGrph  E )
2 uzuzle23 30198 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
3 uznn0sub 10897 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( N  -  2 )  e. 
NN0 )
42, 3syl 16 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e. 
NN0 )
543ad2ant3 1011 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( N  -  2 )  e. 
NN0 )
6 simp2 989 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  X  e.  V )
7 numclwwlk.c . . . . . . . 8  |-  C  =  ( n  e.  NN0  |->  ( ( V ClWWalksN  E ) `
 n ) )
8 numclwwlk.f . . . . . . . 8  |-  F  =  ( v  e.  V ,  n  e.  NN0  |->  { w  e.  ( C `  n )  |  ( w ` 
0 )  =  v } )
97, 8numclwwlkovfel2 30681 . . . . . . 7  |-  ( ( V USGrph  E  /\  ( N  -  2 )  e.  NN0  /\  X  e.  V )  ->  ( P  e.  ( X F ( N  - 
2 ) )  <->  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) ) )
101, 5, 6, 9syl3anc 1218 . . . . . 6  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( P  e.  ( X F ( N  -  2 ) )  <->  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) ) )
11 ccatws1cl 12308 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e. Word  V  /\  X  e.  V )  ->  ( P concat  <" X "> )  e. Word  V
)
1211ex 434 . . . . . . . . . . . . . . . 16  |-  ( P  e. Word  V  ->  ( X  e.  V  ->  ( P concat  <" X "> )  e. Word  V ) )
13123ad2ant1 1009 . . . . . . . . . . . . . . 15  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( X  e.  V  ->  ( P concat  <" X "> )  e. Word  V )
)
14133ad2ant1 1009 . . . . . . . . . . . . . 14  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( X  e.  V  ->  ( P concat  <" X "> )  e. Word  V
) )
1514com12 31 . . . . . . . . . . . . 13  |-  ( X  e.  V  ->  (
( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( P concat  <" X "> )  e. Word  V
) )
16153ad2ant2 1010 . . . . . . . . . . . 12  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( P concat  <" X "> )  e. Word  V
) )
1716imp 429 . . . . . . . . . . 11  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  ->  ( P concat  <" X "> )  e. Word  V
)
1817adantr 465 . . . . . . . . . 10  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  ( P concat  <" X "> )  e. Word  V )
19 nbgraisvtx 23347 . . . . . . . . . . . . . 14  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  Q  e.  V ) )
20 s1cl 12298 . . . . . . . . . . . . . 14  |-  ( Q  e.  V  ->  <" Q ">  e. Word  V )
2119, 20syl6 33 . . . . . . . . . . . . 13  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  <" Q ">  e. Word  V )
)
22213ad2ant1 1009 . . . . . . . . . . . 12  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  <" Q ">  e. Word  V )
)
2322adantr 465 . . . . . . . . . . 11  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  <" Q ">  e. Word  V )
)
2423imp 429 . . . . . . . . . 10  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  <" Q ">  e. Word  V )
25 ccatcl 12279 . . . . . . . . . 10  |-  ( ( ( P concat  <" X "> )  e. Word  V  /\  <" Q ">  e. Word  V )  -> 
( ( P concat  <" X "> ) concat  <" Q "> )  e. Word  V
)
2618, 24, 25syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  (
( P concat  <" X "> ) concat  <" Q "> )  e. Word  V
)
27 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E )  ->  P  e. Word  V )
2827ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( Q  e.  (
<. V ,  E >. Neighbors  X
)  /\  ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  ->  P  e. Word  V )
2928ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  P  e. Word  V )
30 elfzonn0 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  i  e.  NN0 )
3130adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  i  e.  NN0 )
32 lencl 12254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e. Word  V  ->  ( # `
 P )  e. 
NN0 )
33 elfzo0 11592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  <->  ( i  e. 
NN0  /\  ( ( # `
 P )  - 
1 )  e.  NN  /\  i  <  ( (
# `  P )  -  1 ) ) )
34 nn0re 10593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  NN0  ->  i  e.  RR )
3534adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
i  e.  RR )
36 nn0re 10593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
# `  P )  e.  NN0  ->  ( # `  P
)  e.  RR )
37 peano2rem 9680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
# `  P )  e.  RR  ->  ( ( # `
 P )  - 
1 )  e.  RR )
3836, 37syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
# `  P )  e.  NN0  ->  ( ( # `
 P )  - 
1 )  e.  RR )
3938adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( ( # `  P
)  -  1 )  e.  RR )
4036adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( # `  P )  e.  RR )
4135, 39, 403jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( i  e.  RR  /\  ( ( # `  P
)  -  1 )  e.  RR  /\  ( # `
 P )  e.  RR ) )
4236ltm1d 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
# `  P )  e.  NN0  ->  ( ( # `
 P )  - 
1 )  <  ( # `
 P ) )
4342adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( ( # `  P
)  -  1 )  <  ( # `  P
) )
44 lttr 9456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  RR  /\  ( ( # `  P
)  -  1 )  e.  RR  /\  ( # `
 P )  e.  RR )  ->  (
( i  <  (
( # `  P )  -  1 )  /\  ( ( # `  P
)  -  1 )  <  ( # `  P
) )  ->  i  <  ( # `  P
) ) )
4544expcomd 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  RR  /\  ( ( # `  P
)  -  1 )  e.  RR  /\  ( # `
 P )  e.  RR )  ->  (
( ( # `  P
)  -  1 )  <  ( # `  P
)  ->  ( i  <  ( ( # `  P
)  -  1 )  ->  i  <  ( # `
 P ) ) ) )
4641, 43, 45sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( i  <  (
( # `  P )  -  1 )  -> 
i  <  ( # `  P
) ) )
4746impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  i  <  ( ( # `  P )  -  1 ) )  ->  (
( # `  P )  e.  NN0  ->  i  < 
( # `  P ) ) )
48473adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  ( ( # `  P
)  -  1 )  e.  NN  /\  i  <  ( ( # `  P
)  -  1 ) )  ->  ( ( # `
 P )  e. 
NN0  ->  i  <  ( # `
 P ) ) )
4933, 48sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( ( # `
 P )  e. 
NN0  ->  i  <  ( # `
 P ) ) )
5032, 49syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e. Word  V  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  i  <  (
# `  P )
) )
5150ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Q  e.  ( <. V ,  E >. Neighbors  X
)  /\  ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
) )  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  i  <  (
# `  P )
) )
5251ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  i  <  (
# `  P )
) )
5352imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  i  <  (
# `  P )
)
5429, 31, 533jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( P  e. Word  V  /\  i  e. 
NN0  /\  i  <  (
# `  P )
) )
556adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  X  e.  V )
56193ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  Q  e.  V ) )
5756com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  Q  e.  V )
)
5857ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( Q  e.  (
<. V ,  E >. Neighbors  X
)  /\  ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  -> 
( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  ->  Q  e.  V
) )
5958imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  Q  e.  V )
6055, 59jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  ( X  e.  V  /\  Q  e.  V )
)
6160adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( X  e.  V  /\  Q  e.  V ) )
62 ccat2s1fvw 30276 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( P  e. Word  V  /\  i  e.  NN0  /\  i  <  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  i
)  =  ( P `
 i ) )
6362eqcomd 2448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  i  e.  NN0  /\  i  <  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  ( P `  i )  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) )
6454, 61, 63syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( P `  i )  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) )
65 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  P  e. Word  V )
66 peano2nn0 10625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
67663ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  ( ( # `  P
)  -  1 )  e.  NN  /\  i  <  ( ( # `  P
)  -  1 ) )  ->  ( i  +  1 )  e. 
NN0 )
6833, 67sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( i  +  1 )  e. 
NN0 )
6968adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  (
i  +  1 )  e.  NN0 )
70 1re 9390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  1  e.  RR
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
1  e.  RR )
7235, 71, 40ltaddsubd 9944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( ( i  +  1 )  <  ( # `
 P )  <->  i  <  ( ( # `  P
)  -  1 ) ) )
7372biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( i  <  (
( # `  P )  -  1 )  -> 
( i  +  1 )  <  ( # `  P ) ) )
7473impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  i  <  ( ( # `  P )  -  1 ) )  ->  (
( # `  P )  e.  NN0  ->  ( i  +  1 )  < 
( # `  P ) ) )
75743adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  ( ( # `  P
)  -  1 )  e.  NN  /\  i  <  ( ( # `  P
)  -  1 ) )  ->  ( ( # `
 P )  e. 
NN0  ->  ( i  +  1 )  <  ( # `
 P ) ) )
7633, 75sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( ( # `
 P )  e. 
NN0  ->  ( i  +  1 )  <  ( # `
 P ) ) )
7732, 76mpan9 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  (
i  +  1 )  <  ( # `  P
) )
7865, 69, 773jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  ( P  e. Word  V  /\  (
i  +  1 )  e.  NN0  /\  (
i  +  1 )  <  ( # `  P
) ) )
7978ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e. Word  V  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( P  e. Word  V  /\  ( i  +  1 )  e. 
NN0  /\  ( i  +  1 )  < 
( # `  P ) ) ) )
8079ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Q  e.  ( <. V ,  E >. Neighbors  X
)  /\  ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
) )  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( P  e. Word  V  /\  ( i  +  1 )  e. 
NN0  /\  ( i  +  1 )  < 
( # `  P ) ) ) )
8180ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( P  e. Word  V  /\  ( i  +  1 )  e. 
NN0  /\  ( i  +  1 )  < 
( # `  P ) ) ) )
8281imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( P  e. Word  V  /\  ( i  +  1 )  e. 
NN0  /\  ( i  +  1 )  < 
( # `  P ) ) )
83 ccat2s1fvw 30276 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( P  e. Word  V  /\  ( i  +  1 )  e.  NN0  /\  ( i  +  1 )  <  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) )  =  ( P `
 ( i  +  1 ) ) )
8482, 61, 83syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) )  =  ( P `
 ( i  +  1 ) ) )
8584eqcomd 2448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( P `  ( i  +  1 ) )  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) )
8664, 85preq12d 3967 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  =  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) } )
8786eleq1d 2509 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  /\  i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) )  ->  ( {
( P `  i
) ,  ( P `
 ( i  +  1 ) ) }  e.  ran  E  <->  { (
( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
8887ralbidva 2736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  ( A. i  e.  (
0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
8988biimpd 207 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( Q  e.  ( <. V ,  E >. Neighbors  X )  /\  ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E ) )  /\  (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X ) )  /\  ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
) )  ->  ( A. i  e.  (
0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
9089exp41 610 . . . . . . . . . . . . . . . . . . 19  |-  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( P  e. Word  V  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( (
# `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X )  ->  (
( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) )
9190com15 93 . . . . . . . . . . . . . . . . . 18  |-  ( A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  ->  ( ( P  e. Word  V  /\  {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E )  ->  ( (
( # `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X )  ->  (
( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) )
9291expd 436 . . . . . . . . . . . . . . . . 17  |-  ( A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  ->  ( P  e. Word  V  ->  ( { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E  ->  ( ( ( # `  P )  =  ( N  -  2 )  /\  ( P ` 
0 )  =  X )  ->  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) ) )
9392com12 31 . . . . . . . . . . . . . . . 16  |-  ( P  e. Word  V  ->  ( A. i  e.  (
0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  ->  ( {
( lastS  `  P ) ,  ( P `  0
) }  e.  ran  E  ->  ( ( (
# `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X )  ->  (
( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) ) )
94933imp 1181 . . . . . . . . . . . . . . 15  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( (
# `  P )  =  ( N  - 
2 )  /\  ( P `  0 )  =  X )  ->  (
( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) )
95943impib 1185 . . . . . . . . . . . . . 14  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) )
9695impcom 430 . . . . . . . . . . . . 13  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
9796imp 429 . . . . . . . . . . . 12  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E )
98 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  P  e. Word  V
)
99 oveq1 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  P )  =  ( N  - 
2 )  ->  (
( # `  P )  -  1 )  =  ( ( N  - 
2 )  -  1 ) )
10099adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  P
)  =  ( N  -  2 )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  P
)  -  1 )  =  ( ( N  -  2 )  - 
1 ) )
101 eluzelcn 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  CC )
102 2cnd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  CC )
103 ax-1cn 9345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  CC
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  CC )
105101, 102, 104subsub4d 9755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  (
2  +  1 ) ) )
106 2p1e3 10450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 2  +  1 )  =  3
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  +  1 )  =  3 )
108107oveq2d 6112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  =  ( N  -  3 ) )
109 uznn0sub 10897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  e. 
NN0 )
110108, 109eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  e. 
NN0 )
111105, 110eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  e. 
NN0 )
112111adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  P
)  =  ( N  -  2 )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  -  1 )  e.  NN0 )
113100, 112eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  P
)  =  ( N  -  2 )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  P
)  -  1 )  e.  NN0 )
114113adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  ( ( # `  P )  -  1 )  e.  NN0 )
11532, 42syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e. Word  V  ->  (
( # `  P )  -  1 )  < 
( # `  P ) )
116115ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  ( ( # `  P )  -  1 )  <  ( # `  P ) )
11798, 114, 1163jca 1168 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  ( P  e. Word  V  /\  ( ( # `  P )  -  1 )  e.  NN0  /\  ( ( # `  P
)  -  1 )  <  ( # `  P
) ) )
118117exp31 604 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e. Word  V  ->  (
( # `  P )  =  ( N  - 
2 )  ->  ( N  e.  ( ZZ>= ` 
3 )  ->  ( P  e. Word  V  /\  (
( # `  P )  -  1 )  e. 
NN0  /\  ( ( # `
 P )  - 
1 )  <  ( # `
 P ) ) ) ) )
119118a1dd 46 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e. Word  V  ->  (
( # `  P )  =  ( N  - 
2 )  ->  (
( P `  0
)  =  X  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) ) ) ) ) )
1201193ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( # `  P )  =  ( N  -  2 )  ->  ( ( P `
 0 )  =  X  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) ) ) ) ) )
1211203imp 1181 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) ) ) )
122121com12 31 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( (
( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) ) ) )
1231223ad2ant3 1011 . . . . . . . . . . . . . . . . . 18  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) ) ) )
124123imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  ->  ( P  e. Word  V  /\  ( ( # `  P )  -  1 )  e.  NN0  /\  ( ( # `  P
)  -  1 )  <  ( # `  P
) ) )
125124adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  ( P  e. Word  V  /\  (
( # `  P )  -  1 )  e. 
NN0  /\  ( ( # `
 P )  - 
1 )  <  ( # `
 P ) ) )
12619ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( P  e. Word  V  /\  ( V USGrph  E  /\  X  e.  V ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  Q  e.  V ) )
127 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( V USGrph  E  /\  X  e.  V )  ->  X  e.  V )
128127adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( P  e. Word  V  /\  ( V USGrph  E  /\  X  e.  V ) )  ->  X  e.  V )
129126, 128jctild 543 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e. Word  V  /\  ( V USGrph  E  /\  X  e.  V ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( X  e.  V  /\  Q  e.  V ) ) )
130129ex 434 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e. Word  V  ->  (
( V USGrph  E  /\  X  e.  V )  ->  ( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( X  e.  V  /\  Q  e.  V ) ) ) )
1311303ad2ant1 1009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( V USGrph  E  /\  X  e.  V
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  ( X  e.  V  /\  Q  e.  V )
) ) )
1321313ad2ant1 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( ( V USGrph  E  /\  X  e.  V
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  ( X  e.  V  /\  Q  e.  V )
) ) )
133132com12 31 . . . . . . . . . . . . . . . . . 18  |-  ( ( V USGrph  E  /\  X  e.  V )  ->  (
( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( X  e.  V  /\  Q  e.  V ) ) ) )
1341333adant3 1008 . . . . . . . . . . . . . . . . 17  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( X  e.  V  /\  Q  e.  V ) ) ) )
135134imp31 432 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  ( X  e.  V  /\  Q  e.  V )
)
136 ccat2s1fvw 30276 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V ) )  -> 
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( (
# `  P )  -  1 ) )  =  ( P `  ( ( # `  P
)  -  1 ) ) )
137125, 135, 136syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  -  1 ) )  =  ( P `  ( ( # `  P
)  -  1 ) ) )
138 nn0cn 10594 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  P )  e.  NN0  ->  ( # `  P
)  e.  CC )
139 npcan 9624 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( # `  P
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( # `  P )  -  1 )  +  1 )  =  ( # `  P
) )
140138, 103, 139sylancl 662 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  P )  e.  NN0  ->  ( (
( # `  P )  -  1 )  +  1 )  =  (
# `  P )
)
14132, 140syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e. Word  V  ->  (
( ( # `  P
)  -  1 )  +  1 )  =  ( # `  P
) )
1421413ad2ant1 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( (
# `  P )  -  1 )  +  1 )  =  (
# `  P )
)
1431423ad2ant1 1009 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( ( ( # `  P )  -  1 )  +  1 )  =  ( # `  P
) )
144143ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  (
( ( # `  P
)  -  1 )  +  1 )  =  ( # `  P
) )
145144fveq2d 5700 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) )  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) )
146 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  P  e. Word  V
)
147 eqidd 2444 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( # `  P
)  =  ( # `  P ) )
148146, 147jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) ) )
149148adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  -> 
( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) ) )
150127ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  ->  X  e.  V )
15119ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  Q  e.  V ) )
152151imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  ->  Q  e.  V )
153 ccatw2s1p1 30274 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X )
154149, 150, 152, 153syl12anc 1216 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  -> 
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `  P ) )  =  X )
155154ex 434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X ) )
156155expcom 435 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e. Word  V  ->  (
( V USGrph  E  /\  X  e.  V )  ->  ( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
1571563ad2ant1 1009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( V USGrph  E  /\  X  e.  V
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
1581573ad2ant1 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( ( V USGrph  E  /\  X  e.  V
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
159158com12 31 . . . . . . . . . . . . . . . . . 18  |-  ( ( V USGrph  E  /\  X  e.  V )  ->  (
( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
1601593adant3 1008 . . . . . . . . . . . . . . . . 17  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
161160imp31 432 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X )
162145, 161eqtrd 2475 . . . . . . . . . . . . . . 15  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) )  =  X )
163137, 162preq12d 3967 . . . . . . . . . . . . . 14  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  -  1 ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) }  =  { ( P `  ( (
# `  P )  -  1 ) ) ,  X } )
164 lsw 12271 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e. Word  V  ->  ( lastS  `  P )  =  ( P `  ( (
# `  P )  -  1 ) ) )
165164adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( lastS  `  P )  =  ( P `  ( ( # `  P
)  -  1 ) ) )
166 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( P `  0
)  =  X )
167165, 166preq12d 3967 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  { ( lastS  `  P
) ,  ( P `
 0 ) }  =  { ( P `
 ( ( # `  P )  -  1 ) ) ,  X } )
168167eleq1d 2509 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E  <->  { ( P `  ( ( # `
 P )  - 
1 ) ) ,  X }  e.  ran  E ) )
169168biimpd 207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E  ->  { ( P `  ( ( # `  P
)  -  1 ) ) ,  X }  e.  ran  E ) )
170169ex 434 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P `  0 )  =  X  ->  ( P  e. Word  V  ->  ( { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E  ->  { ( P `  ( ( # `
 P )  - 
1 ) ) ,  X }  e.  ran  E ) ) )
171170com3l 81 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e. Word  V  ->  ( { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E  ->  ( ( P `  0 )  =  X  ->  { ( P `  ( (
# `  P )  -  1 ) ) ,  X }  e.  ran  E ) ) )
172171imp 429 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E )  ->  (
( P `  0
)  =  X  ->  { ( P `  ( ( # `  P
)  -  1 ) ) ,  X }  e.  ran  E ) )
1731723adant2 1007 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( P `
 0 )  =  X  ->  { ( P `  ( ( # `
 P )  - 
1 ) ) ,  X }  e.  ran  E ) )
174173a1d 25 . . . . . . . . . . . . . . . 16  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( # `  P )  =  ( N  -  2 )  ->  ( ( P `
 0 )  =  X  ->  { ( P `  ( ( # `
 P )  - 
1 ) ) ,  X }  e.  ran  E ) ) )
1751743imp 1181 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  ->  { ( P `  ( ( # `  P
)  -  1 ) ) ,  X }  e.  ran  E )
176175ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  { ( P `  ( (
# `  P )  -  1 ) ) ,  X }  e.  ran  E )
177163, 176eqeltrd 2517 . . . . . . . . . . . . 13  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  -  1 ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) }  e.  ran  E
)
178 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( # `  P )  =  (
# `  P )
179178, 153mpanl2 681 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( P  e. Word  V  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) )  =  X )
180 ccatw2s1p2 30275 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) )  =  Q )
181178, 180mpanl2 681 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( P  e. Word  V  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) )  =  Q )
182179, 181preq12d 3967 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( P  e. Word  V  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } )
183182expcom 435 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  e.  V  /\  Q  e.  V )  ->  ( P  e. Word  V  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) )
184183expcom 435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  V  ->  ( X  e.  V  ->  ( P  e. Word  V  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
18519, 184syl6 33 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  ( X  e.  V  ->  ( P  e. Word  V  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) ) )
186185com24 87 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V USGrph  E  ->  ( P  e. Word  V  ->  ( X  e.  V  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) ) )
187186com12 31 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e. Word  V  ->  ( V USGrph  E  ->  ( X  e.  V  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) ) )
188187impd 431 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e. Word  V  ->  (
( V USGrph  E  /\  X  e.  V )  ->  ( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  { (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
1891883ad2ant1 1009 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( V USGrph  E  /\  X  e.  V
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
1901893ad2ant1 1009 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( ( V USGrph  E  /\  X  e.  V
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
191190com12 31 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  X  e.  V )  ->  (
( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  { (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
1921913adant3 1008 . . . . . . . . . . . . . . 15  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  { (
( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
193192imp31 432 . . . . . . . . . . . . . 14  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } )
194 nbgraeledg 23346 . . . . . . . . . . . . . . . . . 18  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  <->  { Q ,  X }  e.  ran  E ) )
195 prcom 3958 . . . . . . . . . . . . . . . . . . . 20  |-  { Q ,  X }  =  { X ,  Q }
196195eleq1i 2506 . . . . . . . . . . . . . . . . . . 19  |-  ( { Q ,  X }  e.  ran  E  <->  { X ,  Q }  e.  ran  E )
197196biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( { Q ,  X }  e.  ran  E  ->  { X ,  Q }  e.  ran  E )
198194, 197syl6bi 228 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { X ,  Q }  e.  ran  E ) )
1991983ad2ant1 1009 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { X ,  Q }  e.  ran  E ) )
200199adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { X ,  Q }  e.  ran  E ) )
201200imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  { X ,  Q }  e.  ran  E )
202193, 201eqeltrd 2517 . . . . . . . . . . . . 13  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  e.  ran  E
)
203 ovex 6121 . . . . . . . . . . . . . 14  |-  ( (
# `  P )  -  1 )  e. 
_V
204 fvex 5706 . . . . . . . . . . . . . 14  |-  ( # `  P )  e.  _V
205 fveq2 5696 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  i
)  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  -  1 ) ) )
206 oveq1 6103 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( i  +  1 )  =  ( ( ( # `  P )  -  1 )  +  1 ) )
207206fveq2d 5700 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) )  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) )
208205, 207preq12d 3967 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( # `  P )  -  1 )  ->  { (
( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  =  {
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( (
# `  P )  -  1 ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) } )
209208eleq1d 2509 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( {
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  <->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  -  1 ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) }  e.  ran  E
) )
210 fveq2 5696 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( # `  P
)  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  i
)  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) )
211 oveq1 6103 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( # `  P
)  ->  ( i  +  1 )  =  ( ( # `  P
)  +  1 ) )
212211fveq2d 5700 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( # `  P
)  ->  ( (
( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) )  =  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) )
213210, 212preq12d 3967 . . . . . . . . . . . . . . 15  |-  ( i  =  ( # `  P
)  ->  { (
( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  =  {
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `  P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( (
# `  P )  +  1 ) ) } )
214213eleq1d 2509 . . . . . . . . . . . . . 14  |-  ( i  =  ( # `  P
)  ->  ( {
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  <->  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  e.  ran  E
) )
215203, 204, 209, 214ralpr 3934 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( # `  P )  -  1 ) ,  ( # `  P
) }  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  <-> 
( { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  -  1 ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) }  e.  ran  E  /\  { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  e.  ran  E
) )
216177, 202, 215sylanbrc 664 . . . . . . . . . . . 12  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  A. i  e.  { ( ( # `  P )  -  1 ) ,  ( # `  P ) }  {
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E )
21797, 216jca 532 . . . . . . . . . . 11  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  /\  ( # `  P
)  =  ( N  -  2 )  /\  ( P `  0 )  =  X ) )  /\  Q  e.  (
<. V ,  E >. Neighbors  X
) )  ->  ( A. i  e.  (
0..^ ( ( # `  P )  -  1 ) ) { ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i
) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  /\  A. i  e. 
{ ( ( # `  P )  -  1 ) ,  ( # `  P ) }  {
( ( ( P concat  <" X "> ) concat  <" Q "> ) `  i ) ,  ( ( ( P concat  <" X "> ) concat  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
218 2cnd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  P )  e.  NN0  ->  2  e.  CC )
219103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  P )  e.  NN0  ->  1  e.  CC )
220138, 218, 2193jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  P )  e.  NN0  ->  ( ( # `
 P )  e.  CC  /\  2  e.  CC  /\  1  e.  CC ) )
22132, 220syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e. Word  V  ->  (
( # `  P )  e.  CC  /\  2  e.  CC  /\  1  e.  CC ) )
2222213ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) { ( P `
 i ) ,  ( P `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E )  ->  ( ( # `  P )  e.  CC  /\  2  e.  CC  /\  1  e.  CC )
)
223222adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( P  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  P )  -  1 ) ) { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  P ) ,  ( P `  0 ) }  e.  ran  E
)  /\  ( ( # `
 P )  =  ( N  -  2 )  /\  N  e.  ( ZZ>= `  3 )
) )  ->  (
( # `  P )  e.  CC  /\  2  e.  CC  /\  1  e.  CC ) )
224 addsubass 9625 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  P
)  e.