Metamath Proof Explorer

Theorem clwlkclwwlklem3

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

Ref Expression
Assertion clwlkclwwlklem3 
|- ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> E : dom E -1-1-> R )
2 simp1 
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> f e. Word dom E )
3 2 adantr 
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> f e. Word dom E )
4 1 3 anim12i 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( E : dom E -1-1-> R /\ f e. Word dom E ) )
5 simp3 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) )
6 simpl2 
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> P : ( 0 ... ( # ` f ) ) --> V )
7 5 6 anim12ci 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( P : ( 0 ... ( # ` f ) ) --> V /\ 2 <_ ( # ` P ) ) )
8 simp3 
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
9 8 anim1i 
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) )
10 9 adantl 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) )
11 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 ) )
12 4 7 10 11 syl3anc 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ 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 ) )
13 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
14 lencl 
 |-  ( f e. Word dom E -> ( # ` f ) e. NN0 )
15 ffz0hash 
 |-  ( ( ( # ` f ) e. NN0 /\ P : ( 0 ... ( # ` f ) ) --> V ) -> ( # ` P ) = ( ( # ` f ) + 1 ) )
16 oveq1 
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( # ` P ) - 1 ) = ( ( ( # ` f ) + 1 ) - 1 ) )
17 16 oveq1d 
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( ( # ` P ) - 1 ) - 0 ) = ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) )
18 nn0cn 
 |-  ( ( # ` f ) e. NN0 -> ( # ` f ) e. CC )
19 peano2cn 
 |-  ( ( # ` f ) e. CC -> ( ( # ` f ) + 1 ) e. CC )
20 peano2cnm 
 |-  ( ( ( # ` f ) + 1 ) e. CC -> ( ( ( # ` f ) + 1 ) - 1 ) e. CC )
21 18 19 20 3syl 
 |-  ( ( # ` f ) e. NN0 -> ( ( ( # ` f ) + 1 ) - 1 ) e. CC )
22 21 subid1d 
 |-  ( ( # ` f ) e. NN0 -> ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) = ( ( ( # ` f ) + 1 ) - 1 ) )
23 1cnd 
 |-  ( ( # ` f ) e. NN0 -> 1 e. CC )
24 18 23 pncand 
 |-  ( ( # ` f ) e. NN0 -> ( ( ( # ` f ) + 1 ) - 1 ) = ( # ` f ) )
25 22 24 eqtrd 
 |-  ( ( # ` f ) e. NN0 -> ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) = ( # ` f ) )
26 25 adantr 
 |-  ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) = ( # ` f ) )
27 17 26 sylan9eqr 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( # ` P ) - 1 ) - 0 ) = ( # ` f ) )
28 27 oveq1d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( # ` f ) - 1 ) )
29 28 oveq2d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) = ( 0 ..^ ( ( # ` f ) - 1 ) ) )
30 29 raleqdv 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
31 oveq1 
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( # ` P ) - 2 ) = ( ( ( # ` f ) + 1 ) - 2 ) )
32 2cnd 
 |-  ( ( # ` f ) e. NN0 -> 2 e. CC )
33 18 32 23 subsub3d 
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) - ( 2 - 1 ) ) = ( ( ( # ` f ) + 1 ) - 2 ) )
34 2m1e1 
 |-  ( 2 - 1 ) = 1
35 34 a1i 
 |-  ( ( # ` f ) e. NN0 -> ( 2 - 1 ) = 1 )
36 35 oveq2d 
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) - ( 2 - 1 ) ) = ( ( # ` f ) - 1 ) )
37 33 36 eqtr3d 
 |-  ( ( # ` f ) e. NN0 -> ( ( ( # ` f ) + 1 ) - 2 ) = ( ( # ` f ) - 1 ) )
38 37 adantr 
 |-  ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( # ` f ) + 1 ) - 2 ) = ( ( # ` f ) - 1 ) )
39 31 38 sylan9eqr 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( # ` P ) - 2 ) = ( ( # ` f ) - 1 ) )
40 39 fveq2d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( P ` ( ( # ` P ) - 2 ) ) = ( P ` ( ( # ` f ) - 1 ) ) )
41 40 preq1d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } )
42 41 eleq1d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )
43 30 42 anbi12d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) <-> ( A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) )
44 43 anbi2d 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
45 3anass 
 |-  ( ( ( 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 ) <-> ( ( 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 ) ) )
46 44 45 bitr4di 
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) )
47 46 expcom 
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
48 47 expd 
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( # ` f ) e. NN0 -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) ) )
49 15 48 syl 
 |-  ( ( ( # ` f ) e. NN0 /\ P : ( 0 ... ( # ` f ) ) --> V ) -> ( ( # ` f ) e. NN0 -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) ) )
50 49 ex 
 |-  ( ( # ` f ) e. NN0 -> ( P : ( 0 ... ( # ` f ) ) --> V -> ( ( # ` f ) e. NN0 -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) ) ) )
51 50 com23 
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) e. NN0 -> ( P : ( 0 ... ( # ` f ) ) --> V -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) ) ) )
52 14 14 51 sylc 
 |-  ( f e. Word dom E -> ( P : ( 0 ... ( # ` f ) ) --> V -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) ) )
53 52 imp 
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V ) -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
54 53 3adant3 
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
55 54 adantr 
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
56 13 55 syl5com 
 |-  ( P e. Word V -> ( ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
57 56 3ad2ant2 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) ) )
58 57 imp 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( 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 ) ) )
59 12 58 mpbird 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) )
60 59 ex 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
61 60 exlimdv 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
62 clwlkclwwlklem1 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) )
63 61 62 impbid 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ 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 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )