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

Theorem numclwwlkovf2ex 25490
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 ++  <" X "> ) ++  <" 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 997 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  V USGrph  E )
2 uzuzle23 11166 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
3 uznn0sub 11157 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( N  -  2 )  e. 
NN0 )
42, 3syl 17 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e. 
NN0 )
543ad2ant3 1020 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( N  -  2 )  e. 
NN0 )
6 simp2 998 . . . . . . 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 25487 . . . . . . 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 1230 . . . . . 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 12676 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e. Word  V  /\  X  e.  V )  ->  ( P ++  <" X "> )  e. Word  V
)
1211ex 432 . . . . . . . . . . . . . . . 16  |-  ( P  e. Word  V  ->  ( X  e.  V  ->  ( P ++  <" X "> )  e. Word  V ) )
13123ad2ant1 1018 . . . . . . . . . . . . . . 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 ++  <" X "> )  e. Word  V )
)
14133ad2ant1 1018 . . . . . . . . . . . . . 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 ++  <" X "> )  e. Word  V
) )
1514com12 29 . . . . . . . . . . . . 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 ++  <" X "> )  e. Word  V
) )
16153ad2ant2 1019 . . . . . . . . . . . 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 ++  <" X "> )  e. Word  V
) )
1716imp 427 . . . . . . . . . . 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 ++  <" X "> )  e. Word  V )
1817adantr 463 . . . . . . . . . 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 ++  <" X "> )  e. Word  V )
19 nbgraisvtx 24835 . . . . . . . . . . . . . 14  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  Q  e.  V ) )
20 s1cl 12666 . . . . . . . . . . . . . 14  |-  ( Q  e.  V  ->  <" Q ">  e. Word  V )
2119, 20syl6 31 . . . . . . . . . . . . 13  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  <" Q ">  e. Word  V )
)
22213ad2ant1 1018 . . . . . . . . . . . 12  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  <" Q ">  e. Word  V )
)
2322adantr 463 . . . . . . . . . . 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 427 . . . . . . . . . 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 12645 . . . . . . . . . 10  |-  ( ( ( P ++  <" X "> )  e. Word  V  /\  <" Q ">  e. Word  V )  -> 
( ( P ++  <" X "> ) ++  <" Q "> )  e. Word  V )
2618, 24, 25syl2anc 659 . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> )  e. Word  V
)
27 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E )  ->  P  e. Word  V )
2827ad2antlr 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 ) )  ->  P  e. Word  V )
2928ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  i  e.  NN0 )
3130adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 12612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e. Word  V  ->  ( # `
 P )  e. 
NN0 )
33 elfzo0 11893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  <->  ( i  e. 
NN0  /\  ( ( # `
 P )  - 
1 )  e.  NN  /\  i  <  ( (
# `  P )  -  1 ) ) )
34 nn0re 10844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  NN0  ->  i  e.  RR )
3534adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
i  e.  RR )
36 nn0re 10844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
# `  P )  e.  NN0  ->  ( # `  P
)  e.  RR )
37 peano2rem 9921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
# `  P )  e.  RR  ->  ( ( # `
 P )  - 
1 )  e.  RR )
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
# `  P )  e.  NN0  ->  ( ( # `
 P )  - 
1 )  e.  RR )
3938adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( ( # `  P
)  -  1 )  e.  RR )
4036adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( # `  P )  e.  RR )
4135, 39, 403jca 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( i  e.  RR  /\  ( ( # `  P
)  -  1 )  e.  RR  /\  ( # `
 P )  e.  RR ) )
4236ltm1d 10517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
# `  P )  e.  NN0  ->  ( ( # `
 P )  - 
1 )  <  ( # `
 P ) )
4342adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( ( # `  P
)  -  1 )  <  ( # `  P
) )
44 lttr 9691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  RR  /\  ( ( # `  P
)  -  1 )  e.  RR  /\  ( # `
 P )  e.  RR )  ->  (
( i  <  (
( # `  P )  -  1 )  /\  ( ( # `  P
)  -  1 )  <  ( # `  P
) )  ->  i  <  ( # `  P
) ) )
4544expcomd 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  RR  /\  ( ( # `  P
)  -  1 )  e.  RR  /\  ( # `
 P )  e.  RR )  ->  (
( ( # `  P
)  -  1 )  <  ( # `  P
)  ->  ( i  <  ( ( # `  P
)  -  1 )  ->  i  <  ( # `
 P ) ) ) )
4641, 43, 45sylc 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( i  <  (
( # `  P )  -  1 )  -> 
i  <  ( # `  P
) ) )
4746impancom 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  i  <  ( ( # `  P )  -  1 ) )  ->  (
( # `  P )  e.  NN0  ->  i  < 
( # `  P ) ) )
48473adant2 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e. Word  V  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  i  <  (
# `  P )
) )
5150ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 427 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1177 . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  Q  e.  V ) )
5756com12 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  Q  e.  V )
)
5857ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 427 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 530 . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . 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 12694 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( P  e. Word  V  /\  i  e.  NN0  /\  i  <  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  i )  =  ( P `  i ) )
6362eqcomd 2410 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  i  e.  NN0  /\  i  <  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  ( P `  i )  =  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  i
) )
6454, 61, 63syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i )
)
65 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  P  e. Word  V )
66 peano2nn0 10876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
67663ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  (
i  +  1 )  e.  NN0 )
70 1red 9640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
1  e.  RR )
7135, 70, 40ltaddsubd 10191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( ( i  +  1 )  <  ( # `
 P )  <->  i  <  ( ( # `  P
)  -  1 ) ) )
7271biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  ( # `  P )  e.  NN0 )  -> 
( i  <  (
( # `  P )  -  1 )  -> 
( i  +  1 )  <  ( # `  P ) ) )
7372impancom 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  i  <  ( ( # `  P )  -  1 ) )  ->  (
( # `  P )  e.  NN0  ->  ( i  +  1 )  < 
( # `  P ) ) )
74733adant2 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  ( ( # `  P
)  -  1 )  e.  NN  /\  i  <  ( ( # `  P
)  -  1 ) )  ->  ( ( # `
 P )  e. 
NN0  ->  ( i  +  1 )  <  ( # `
 P ) ) )
7533, 74sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( ( # `
 P )  e. 
NN0  ->  ( i  +  1 )  <  ( # `
 P ) ) )
7632, 75mpan9 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  (
i  +  1 )  <  ( # `  P
) )
7765, 69, 763jca 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( P  e. Word  V  /\  i  e.  ( 0..^ ( ( # `  P
)  -  1 ) ) )  ->  ( P  e. Word  V  /\  (
i  +  1 )  e.  NN0  /\  (
i  +  1 )  <  ( # `  P
) ) )
7877ex 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e. Word  V  ->  (
i  e.  ( 0..^ ( ( # `  P
)  -  1 ) )  ->  ( P  e. Word  V  /\  ( i  +  1 )  e. 
NN0  /\  ( i  +  1 )  < 
( # `  P ) ) ) )
7978ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8079ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8180imp 427 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
82 ccat2s1fvw 12694 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( P  e. Word  V  /\  ( i  +  1 )  e.  NN0  /\  ( i  +  1 )  <  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( i  +  1 ) )  =  ( P `  ( i  +  1 ) ) )
8381, 61, 82syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) )  =  ( P `
 ( i  +  1 ) ) )
8483eqcomd 2410 . . . . . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( i  +  1 ) ) )
8564, 84preq12d 4058 . . . . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) } )
8685eleq1d 2471 . . . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
8786ralbidva 2839 . . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
8887biimpd 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
8988exp41 608 . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) )
9089com15 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) )
9190expd 434 . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) ) )
9291com12 29 . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) ) ) )
93923imp 1191 . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) ) )
94933impib 1195 . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) ) )
9594impcom 428 . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
9695imp 427 . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i
) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E )
97 simpll 752 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  P  e. Word  V
)
98 oveq1 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  P )  =  ( N  - 
2 )  ->  (
( # `  P )  -  1 )  =  ( ( N  - 
2 )  -  1 ) )
9998adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  P
)  =  ( N  -  2 )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  P
)  -  1 )  =  ( ( N  -  2 )  - 
1 ) )
100 eluzelcn 11137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  CC )
101 2cnd 10648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  CC )
102 1cnd 9641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  CC )
103100, 101, 102subsub4d 9997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  (
2  +  1 ) ) )
104 2p1e3 10699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 2  +  1 )  =  3
105104a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  +  1 )  =  3 )
106105oveq2d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  =  ( N  -  3 ) )
107 uznn0sub 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  e. 
NN0 )
108106, 107eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  e. 
NN0 )
109103, 108eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  e. 
NN0 )
110109adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  P
)  =  ( N  -  2 )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  -  1 )  e.  NN0 )
11199, 110eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  P
)  =  ( N  -  2 )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  P
)  -  1 )  e.  NN0 )
112111adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  ( ( # `  P )  -  1 )  e.  NN0 )
11332, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e. Word  V  ->  (
( # `  P )  -  1 )  < 
( # `  P ) )
114113ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  ( ( # `  P )  -  1 )  <  ( # `  P ) )
11597, 112, 1143jca 1177 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( N  -  2 ) )  /\  N  e.  (
ZZ>= `  3 ) )  ->  ( P  e. Word  V  /\  ( ( # `  P )  -  1 )  e.  NN0  /\  ( ( # `  P
)  -  1 )  <  ( # `  P
) ) )
116115exp31 602 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e. Word  V  ->  (
( # `  P )  =  ( N  - 
2 )  ->  ( N  e.  ( ZZ>= ` 
3 )  ->  ( P  e. Word  V  /\  (
( # `  P )  -  1 )  e. 
NN0  /\  ( ( # `
 P )  - 
1 )  <  ( # `
 P ) ) ) ) )
117116a1dd 44 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
1181173ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
1191183imp 1191 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
120119com12 29 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
1211203ad2ant3 1020 . . . . . . . . . . . . . . . . . 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 ) ) ) )
122121imp 427 . . . . . . . . . . . . . . . . 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
) ) )
123122adantr 463 . . . . . . . . . . . . . . . 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 ) ) )
12419ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( P  e. Word  V  /\  ( V USGrph  E  /\  X  e.  V ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  Q  e.  V ) )
125 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( V USGrph  E  /\  X  e.  V )  ->  X  e.  V )
126125adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( P  e. Word  V  /\  ( V USGrph  E  /\  X  e.  V ) )  ->  X  e.  V )
127124, 126jctild 541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e. Word  V  /\  ( V USGrph  E  /\  X  e.  V ) )  -> 
( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( X  e.  V  /\  Q  e.  V ) ) )
128127ex 432 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e. Word  V  ->  (
( V USGrph  E  /\  X  e.  V )  ->  ( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( X  e.  V  /\  Q  e.  V ) ) ) )
1291283ad2ant1 1018 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
1301293ad2ant1 1018 . . . . . . . . . . . . . . . . . . 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 )
) ) )
131130com12 29 . . . . . . . . . . . . . . . . . 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 ) ) ) )
1321313adant3 1017 . . . . . . . . . . . . . . . . 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 ) ) ) )
133132imp31 430 . . . . . . . . . . . . . . . 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 )
)
134 ccat2s1fvw 12694 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  e. Word  V  /\  ( ( # `  P
)  -  1 )  e.  NN0  /\  (
( # `  P )  -  1 )  < 
( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V ) )  -> 
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( (
# `  P )  -  1 ) )  =  ( P `  ( ( # `  P
)  -  1 ) ) )
135123, 133, 134syl2anc 659 . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  - 
1 ) )  =  ( P `  (
( # `  P )  -  1 ) ) )
136 nn0cn 10845 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  P )  e.  NN0  ->  ( # `  P
)  e.  CC )
137 ax-1cn 9579 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
138 npcan 9864 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( # `  P
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( # `  P )  -  1 )  +  1 )  =  ( # `  P
) )
139136, 137, 138sylancl 660 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  P )  e.  NN0  ->  ( (
( # `  P )  -  1 )  +  1 )  =  (
# `  P )
)
14032, 139syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e. Word  V  ->  (
( ( # `  P
)  -  1 )  +  1 )  =  ( # `  P
) )
1411403ad2ant1 1018 . . . . . . . . . . . . . . . . . . 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 )
)
1421413ad2ant1 1018 . . . . . . . . . . . . . . . . . 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
) )
143142ad2antlr 725 . . . . . . . . . . . . . . . . 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
) )
144143fveq2d 5852 . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( (
( # `  P )  -  1 )  +  1 ) )  =  ( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( # `  P ) ) )
145 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  P  e. Word  V
)
146 eqidd 2403 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( # `  P
)  =  ( # `  P ) )
147145, 146jca 530 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) ) )
148147adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  -> 
( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) ) )
149125ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  ->  X  e.  V )
15019ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  Q  e.  V ) )
151150imp 427 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  ->  Q  e.  V )
152 ccatw2s1p1 12692 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) )  =  X )
153148, 149, 151, 152syl12anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( V USGrph  E  /\  X  e.  V
)  /\  P  e. Word  V )  /\  Q  e.  ( <. V ,  E >. Neighbors  X ) )  -> 
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( # `  P ) )  =  X )
154153ex 432 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( V USGrph  E  /\  X  e.  V )  /\  P  e. Word  V )  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) )  =  X ) )
155154expcom 433 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e. Word  V  ->  (
( V USGrph  E  /\  X  e.  V )  ->  ( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  ( (
( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
1561553ad2ant1 1018 . . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) )  =  X ) ) )
1571563ad2ant1 1018 . . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) )  =  X ) ) )
158157com12 29 . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
1591583adant3 1017 . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) )  =  X ) ) )
160159imp31 430 . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) )  =  X )
161144, 160eqtrd 2443 . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( (
( # `  P )  -  1 )  +  1 ) )  =  X )
162135, 161preq12d 4058 . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  - 
1 ) ) ,  ( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( ( ( # `  P
)  -  1 )  +  1 ) ) }  =  { ( P `  ( (
# `  P )  -  1 ) ) ,  X } )
163 lsw 12636 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e. Word  V  ->  ( lastS  `  P )  =  ( P `  ( (
# `  P )  -  1 ) ) )
164163adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( lastS  `  P )  =  ( P `  ( ( # `  P
)  -  1 ) ) )
165 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( P `  0
)  =  X )
166164, 165preq12d 4058 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  { ( lastS  `  P
) ,  ( P `
 0 ) }  =  { ( P `
 ( ( # `  P )  -  1 ) ) ,  X } )
167166eleq1d 2471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E  <->  { ( P `  ( ( # `
 P )  - 
1 ) ) ,  X }  e.  ran  E ) )
168167biimpd 207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P `  0
)  =  X  /\  P  e. Word  V )  ->  ( { ( lastS  `  P
) ,  ( P `
 0 ) }  e.  ran  E  ->  { ( P `  ( ( # `  P
)  -  1 ) ) ,  X }  e.  ran  E ) )
169168ex 432 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P `  0 )  =  X  ->  ( P  e. Word  V  ->  ( { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E  ->  { ( P `  ( ( # `
 P )  - 
1 ) ) ,  X }  e.  ran  E ) ) )
170169com3l 81 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e. Word  V  ->  ( { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E  ->  ( ( P `  0 )  =  X  ->  { ( P `  ( (
# `  P )  -  1 ) ) ,  X }  e.  ran  E ) ) )
171170imp 427 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e. Word  V  /\  { ( lastS  `  P ) ,  ( P ` 
0 ) }  e.  ran  E )  ->  (
( P `  0
)  =  X  ->  { ( P `  ( ( # `  P
)  -  1 ) ) ,  X }  e.  ran  E ) )
1721713adant2 1016 . . . . . . . . . . . . . . . . 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 ) )
173172a1d 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 ) ) )
1741733imp 1191 . . . . . . . . . . . . . . 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 )
175174ad2antlr 725 . . . . . . . . . . . . . 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 )
176162, 175eqeltrd 2490 . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  - 
1 ) ) ,  ( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( ( ( # `  P
)  -  1 )  +  1 ) ) }  e.  ran  E
)
177 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( # `  P )  =  (
# `  P )
178177, 152mpanl2 679 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( P  e. Word  V  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) )  =  X )
179 ccatw2s1p2 12693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( P  e. Word  V  /\  ( # `  P
)  =  ( # `  P ) )  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) )  =  Q )
180177, 179mpanl2 679 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( P  e. Word  V  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) )  =  Q )
181178, 180preq12d 4058 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( P  e. Word  V  /\  ( X  e.  V  /\  Q  e.  V
) )  ->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } )
182181expcom 433 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  e.  V  /\  Q  e.  V )  ->  ( P  e. Word  V  ->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) )
183182expcom 433 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  V  ->  ( X  e.  V  ->  ( P  e. Word  V  ->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) )
18419, 183syl6 31 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  ( X  e.  V  ->  ( P  e. Word  V  ->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  =  { X ,  Q } ) ) ) )
185184com24 87 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V USGrph  E  ->  ( P  e. Word  V  ->  ( X  e.  V  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) ) )
186185com12 29 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e. Word  V  ->  ( V USGrph  E  ->  ( X  e.  V  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) ) )
187186impd 429 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e. Word  V  ->  (
( V USGrph  E  /\  X  e.  V )  ->  ( Q  e.  (
<. V ,  E >. Neighbors  X
)  ->  { (
( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) )
1881873ad2ant1 1018 . . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) )
1891883ad2ant1 1018 . . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) )
190189com12 29 . . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) )
1911903adant3 1017 . . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } ) ) )
192191imp31 430 . . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  =  { X ,  Q } )
193 nbgraeledg 24834 . . . . . . . . . . . . . . . . . 18  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  <->  { Q ,  X }  e.  ran  E ) )
194 prcom 4049 . . . . . . . . . . . . . . . . . . . 20  |-  { Q ,  X }  =  { X ,  Q }
195194eleq1i 2479 . . . . . . . . . . . . . . . . . . 19  |-  ( { Q ,  X }  e.  ran  E  <->  { X ,  Q }  e.  ran  E )
196195biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( { Q ,  X }  e.  ran  E  ->  { X ,  Q }  e.  ran  E )
197193, 196syl6bi 228 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { X ,  Q }  e.  ran  E ) )
1981973ad2ant1 1018 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( Q  e.  ( <. V ,  E >. Neighbors  X )  ->  { X ,  Q }  e.  ran  E ) )
199198adantr 463 . . . . . . . . . . . . . . 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 ) )
200199imp 427 . . . . . . . . . . . . . 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 )
201192, 200eqeltrd 2490 . . . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  ( # `  P
) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( ( # `
 P )  +  1 ) ) }  e.  ran  E )
202 ovex 6305 . . . . . . . . . . . . . 14  |-  ( (
# `  P )  -  1 )  e. 
_V
203 fvex 5858 . . . . . . . . . . . . . 14  |-  ( # `  P )  e.  _V
204 fveq2 5848 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( (
( P ++  <" X "> ) ++  <" Q "> ) `  i
)  =  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  -  1 ) ) )
205 oveq1 6284 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( i  +  1 )  =  ( ( ( # `  P )  -  1 )  +  1 ) )
206205fveq2d 5852 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( (
( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) )  =  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) )
207204, 206preq12d 4058 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( # `  P )  -  1 )  ->  { (
( ( P ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  =  {
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( (
# `  P )  -  1 ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) } )
208207eleq1d 2471 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( # `  P )  -  1 )  ->  ( {
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  <->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  -  1 ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) }  e.  ran  E
) )
209 fveq2 5848 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( # `  P
)  ->  ( (
( P ++  <" X "> ) ++  <" Q "> ) `  i
)  =  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) ) )
210 oveq1 6284 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( # `  P
)  ->  ( i  +  1 )  =  ( ( # `  P
)  +  1 ) )
211210fveq2d 5852 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( # `  P
)  ->  ( (
( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) )  =  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  +  1 ) ) )
212209, 211preq12d 4058 . . . . . . . . . . . . . . 15  |-  ( i  =  ( # `  P
)  ->  { (
( ( P ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  =  {
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( # `  P ) ) ,  ( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  ( (
# `  P )  +  1 ) ) } )
213212eleq1d 2471 . . . . . . . . . . . . . 14  |-  ( i  =  ( # `  P
)  ->  ( {
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  <->  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  e.  ran  E
) )
214202, 203, 208, 213ralpr 4024 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( # `  P )  -  1 ) ,  ( # `  P
) }  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  <-> 
( { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  -  1 ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( ( # `  P
)  -  1 )  +  1 ) ) }  e.  ran  E  /\  { ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  ( # `
 P ) ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
( # `  P )  +  1 ) ) }  e.  ran  E
) )
215176, 201, 214sylanbrc 662 . . . . . . . . . . . 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 ++ 
<" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E )
21696, 215jca 530 . . . . . . . . . . 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 ++  <" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E  /\  A. i  e. 
{ ( ( # `  P )  -  1 ) ,  ( # `  P ) }  {
( ( ( P ++ 
<" X "> ) ++  <" Q "> ) `  i ) ,  ( ( ( P ++  <" X "> ) ++  <" Q "> ) `  (
i  +  1 ) ) }  e.  ran  E ) )
217 2cnd 10648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  P )  e.  NN0  ->  2  e.  CC )
218 1cnd 9641 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  P )  e.  NN0  ->  1  e.  CC )
219136, 217, 2183jca 1177 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  P )  e.  NN0  ->  ( ( # `
 P )  e.  CC  /\  2  e.  CC  /\  1  e.  CC ) )
22032, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e. Word  V  ->  (
( # `  P )  e.  CC  /\  2  e.  CC  /\  1  e.  CC ) )
2212203ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
222221adantr 463 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
223 addsubass 9865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  P
)  e.  CC  /\  2  e.  CC  /\  1  e.  CC )  ->  (
( ( # `  P
)  +  2 )  -  1 )  =  ( ( # `  P
)