This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwlkclwwlklem2

Description: Lemma 2 for clwlkclwwlk . (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem2 
|- ( ( ( E : dom E -1-1-> R /\ F e. Word dom E ) /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ 2 <_ ( # ` P ) ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )

Proof

Step Hyp Ref Expression
1 f1fn 
 |-  ( E : dom E -1-1-> R -> E Fn dom E )
2 dffn3 
 |-  ( E Fn dom E <-> E : dom E --> ran E )
3 1 2 sylib 
 |-  ( E : dom E -1-1-> R -> E : dom E --> ran E )
4 lencl 
 |-  ( F e. Word dom E -> ( # ` F ) e. NN0 )
5 ffn 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P Fn ( 0 ... ( # ` F ) ) )
6 fnfz0hash 
 |-  ( ( ( # ` F ) e. NN0 /\ P Fn ( 0 ... ( # ` F ) ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) )
7 4 5 6 syl2an 
 |-  ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( # ` P ) = ( ( # ` F ) + 1 ) )
8 ffz0iswrd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P e. Word V )
9 lsw 
 |-  ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
10 9 ad6antr 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
11 fvoveq1 
 |-  ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) )
12 11 ad4antlr 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) )
13 eqcom 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` ( # ` F ) ) = ( P ` 0 ) )
14 nn0cn 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC )
15 1cnd 
 |-  ( ( # ` F ) e. NN0 -> 1 e. CC )
16 14 15 pncand 
 |-  ( ( # ` F ) e. NN0 -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
17 16 eqcomd 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) = ( ( ( # ` F ) + 1 ) - 1 ) )
18 17 ad4antlr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( # ` F ) = ( ( ( # ` F ) + 1 ) - 1 ) )
19 18 fveqeq2d 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( P ` ( # ` F ) ) = ( P ` 0 ) <-> ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) = ( P ` 0 ) ) )
20 19 biimpd 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( P ` ( # ` F ) ) = ( P ` 0 ) -> ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) = ( P ` 0 ) ) )
21 13 20 biimtrid 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) = ( P ` 0 ) ) )
22 21 adantld 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) = ( P ` 0 ) ) )
23 22 imp 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( P ` ( ( ( # ` F ) + 1 ) - 1 ) ) = ( P ` 0 ) )
24 10 12 23 3eqtrd 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( lastS ` P ) = ( P ` 0 ) )
25 nn0z 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
26 peano2zm 
 |-  ( ( # ` F ) e. ZZ -> ( ( # ` F ) - 1 ) e. ZZ )
27 25 26 syl 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) - 1 ) e. ZZ )
28 nn0re 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. RR )
29 28 lem1d 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) - 1 ) <_ ( # ` F ) )
30 eluz2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) <-> ( ( ( # ` F ) - 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( ( # ` F ) - 1 ) <_ ( # ` F ) ) )
31 27 25 29 30 syl3anbrc 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
32 31 ad4antlr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
33 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
34 ssralv 
 |-  ( ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
35 32 33 34 3syl 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
36 simpr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> E : dom E --> ran E )
37 36 adantr 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> E : dom E --> ran E )
38 wrdf 
 |-  ( F e. Word dom E -> F : ( 0 ..^ ( # ` F ) ) --> dom E )
39 simpll 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) --> dom E /\ ( # ` F ) e. NN0 ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> F : ( 0 ..^ ( # ` F ) ) --> dom E )
40 fzossrbm1 
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
41 25 40 syl 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
42 41 adantl 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> dom E /\ ( # ` F ) e. NN0 ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
43 42 sselda 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) --> dom E /\ ( # ` F ) e. NN0 ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
44 39 43 ffvelcdmd 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) --> dom E /\ ( # ` F ) e. NN0 ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( F ` i ) e. dom E )
45 44 exp31 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom E -> ( ( # ` F ) e. NN0 -> ( i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( F ` i ) e. dom E ) ) )
46 38 45 syl 
 |-  ( F e. Word dom E -> ( ( # ` F ) e. NN0 -> ( i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( F ` i ) e. dom E ) ) )
47 46 adantl 
 |-  ( ( P e. Word V /\ F e. Word dom E ) -> ( ( # ` F ) e. NN0 -> ( i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( F ` i ) e. dom E ) ) )
48 47 imp 
 |-  ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) -> ( i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( F ` i ) e. dom E ) )
49 48 ad3antrrr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( F ` i ) e. dom E ) )
50 49 imp 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( F ` i ) e. dom E )
51 37 50 ffvelcdmd 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( E ` ( F ` i ) ) e. ran E )
52 eqcom 
 |-  ( ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( E ` ( F ` i ) ) )
53 52 biimpi 
 |-  ( ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( E ` ( F ` i ) ) )
54 53 eleq1d 
 |-  ( ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> ( E ` ( F ` i ) ) e. ran E ) )
55 51 54 syl5ibrcom 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
56 55 ralimdva 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
57 35 56 syldc 
 |-  ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
58 57 adantr 
 |-  ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
59 58 impcom 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E )
60 breq2 
 |-  ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) <-> 2 <_ ( ( # ` F ) + 1 ) ) )
61 60 adantl 
 |-  ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( 2 <_ ( # ` P ) <-> 2 <_ ( ( # ` F ) + 1 ) ) )
62 2re 
 |-  2 e. RR
63 62 a1i 
 |-  ( ( # ` F ) e. NN0 -> 2 e. RR )
64 1red 
 |-  ( ( # ` F ) e. NN0 -> 1 e. RR )
65 63 64 28 lesubaddd 
 |-  ( ( # ` F ) e. NN0 -> ( ( 2 - 1 ) <_ ( # ` F ) <-> 2 <_ ( ( # ` F ) + 1 ) ) )
66 2m1e1 
 |-  ( 2 - 1 ) = 1
67 66 breq1i 
 |-  ( ( 2 - 1 ) <_ ( # ` F ) <-> 1 <_ ( # ` F ) )
68 elnnnn0c 
 |-  ( ( # ` F ) e. NN <-> ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) )
69 68 simplbi2 
 |-  ( ( # ` F ) e. NN0 -> ( 1 <_ ( # ` F ) -> ( # ` F ) e. NN ) )
70 67 69 biimtrid 
 |-  ( ( # ` F ) e. NN0 -> ( ( 2 - 1 ) <_ ( # ` F ) -> ( # ` F ) e. NN ) )
71 65 70 sylbird 
 |-  ( ( # ` F ) e. NN0 -> ( 2 <_ ( ( # ` F ) + 1 ) -> ( # ` F ) e. NN ) )
72 71 adantl 
 |-  ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) -> ( 2 <_ ( ( # ` F ) + 1 ) -> ( # ` F ) e. NN ) )
73 72 adantr 
 |-  ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( 2 <_ ( ( # ` F ) + 1 ) -> ( # ` F ) e. NN ) )
74 61 73 sylbid 
 |-  ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( 2 <_ ( # ` P ) -> ( # ` F ) e. NN ) )
75 74 imp 
 |-  ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) -> ( # ` F ) e. NN )
76 75 adantr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( # ` F ) e. NN )
77 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
78 76 77 sylibr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
79 fzoend 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
80 78 79 syl 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
81 2fveq3 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( E ` ( F ` i ) ) = ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) )
82 fveq2 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( P ` i ) = ( P ` ( ( # ` F ) - 1 ) ) )
83 fvoveq1 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( P ` ( i + 1 ) ) = ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) )
84 82 83 preq12d 
 |-  ( i = ( ( # ` F ) - 1 ) -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } )
85 81 84 eqeq12d 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } ) )
86 85 adantl 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ i = ( ( # ` F ) - 1 ) ) -> ( ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } ) )
87 80 86 rspcdv 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } ) )
88 14 15 npcand 
 |-  ( ( # ` F ) e. NN0 -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
89 88 ad4antlr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
90 89 fveq2d 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) = ( P ` ( # ` F ) ) )
91 90 preq2d 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } )
92 91 eqeq2d 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } <-> ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } ) )
93 38 ad4antlr 
 |-  ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) -> F : ( 0 ..^ ( # ` F ) ) --> dom E )
94 71 com12 
 |-  ( 2 <_ ( ( # ` F ) + 1 ) -> ( ( # ` F ) e. NN0 -> ( # ` F ) e. NN ) )
95 60 94 biimtrdi 
 |-  ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( ( # ` F ) e. NN0 -> ( # ` F ) e. NN ) ) )
96 95 com3r 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( # ` F ) e. NN ) ) )
97 96 adantl 
 |-  ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( # ` F ) e. NN ) ) )
98 97 imp31 
 |-  ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) -> ( # ` F ) e. NN )
99 98 77 sylibr 
 |-  ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
100 99 79 syl 
 |-  ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
101 93 100 ffvelcdmd 
 |-  ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) -> ( F ` ( ( # ` F ) - 1 ) ) e. dom E )
102 101 adantr 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( F ` ( ( # ` F ) - 1 ) ) e. dom E )
103 36 102 ffvelcdmd 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) e. ran E )
104 eqcom 
 |-  ( ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } <-> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } = ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) )
105 104 biimpi 
 |-  ( ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } = ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) )
106 105 eleq1d 
 |-  ( ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } -> ( { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E <-> ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) e. ran E ) )
107 103 106 syl5ibrcom 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
108 92 107 sylbid 
 |-  ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> ( ( E ` ( F ` ( ( # ` F ) - 1 ) ) ) = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
109 87 108 syldc 
 |-  ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
110 109 adantr 
 |-  ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
111 110 impcom 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E )
112 preq2 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } )
113 112 eleq1d 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
114 113 adantl 
 |-  ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
115 114 adantl 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( # ` F ) ) } e. ran E ) )
116 111 115 mpbird 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E )
117 24 59 116 3jca 
 |-  ( ( ( ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) /\ 2 <_ ( # ` P ) ) /\ E : dom E --> ran E ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )
118 117 exp41 
 |-  ( ( ( ( P e. Word V /\ F e. Word dom E ) /\ ( # ` F ) e. NN0 ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) )
119 118 exp41 
 |-  ( P e. Word V -> ( F e. Word dom E -> ( ( # ` F ) e. NN0 -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) ) ) )
120 8 119 syl 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> ( F e. Word dom E -> ( ( # ` F ) e. NN0 -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) ) ) )
121 120 com13 
 |-  ( ( # ` F ) e. NN0 -> ( F e. Word dom E -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) ) ) )
122 4 121 mpcom 
 |-  ( F e. Word dom E -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) ) )
123 122 imp 
 |-  ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) )
124 7 123 mpd 
 |-  ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) )
125 124 expcom 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> ( F e. Word dom E -> ( 2 <_ ( # ` P ) -> ( E : dom E --> ran E -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) )
126 125 com14 
 |-  ( E : dom E --> ran E -> ( F e. Word dom E -> ( 2 <_ ( # ` P ) -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) )
127 126 imp 
 |-  ( ( E : dom E --> ran E /\ F e. Word dom E ) -> ( 2 <_ ( # ` P ) -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) )
128 127 impcomd 
 |-  ( ( E : dom E --> ran E /\ F e. Word dom E ) -> ( ( P : ( 0 ... ( # ` F ) ) --> V /\ 2 <_ ( # ` P ) ) -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
129 3 128 sylan 
 |-  ( ( E : dom E -1-1-> R /\ F e. Word dom E ) -> ( ( P : ( 0 ... ( # ` F ) ) --> V /\ 2 <_ ( # ` P ) ) -> ( ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
130 129 3imp 
 |-  ( ( ( E : dom E -1-1-> R /\ F e. Word dom E ) /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ 2 <_ ( # ` P ) ) /\ ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )