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

Metamath Proof Explorer

Theorem clwlkclwwlk

Description: A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlk.v 
|- V = ( Vtx ` G )
clwlkclwwlk.e 
|- E = ( iEdg ` G )
Assertion clwlkclwwlk 
|- ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f f ( ClWalks ` G ) P <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( P prefix ( ( # ` P ) - 1 ) ) e. ( ClWWalks ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlk.v 
 |-  V = ( Vtx ` G )
2 clwlkclwwlk.e 
 |-  E = ( iEdg ` G )
3 2 uspgrf1oedg 
 |-  ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )
4 f1of1 
 |-  ( E : dom E -1-1-onto-> ( Edg ` G ) -> E : dom E -1-1-> ( Edg ` G ) )
5 3 4 syl 
 |-  ( G e. USPGraph -> E : dom E -1-1-> ( Edg ` G ) )
6 clwlkclwwlklem3 
 |-  ( ( E : dom E -1-1-> ( Edg ` G ) /\ 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 ) ) ) )
7 5 6 syl3an1 
 |-  ( ( G e. USPGraph /\ 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 ) ) ) )
8 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
9 ige2m1fz 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. ( 0 ... ( # ` P ) ) )
10 8 9 sylan 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. ( 0 ... ( # ` P ) ) )
11 pfxlen 
 |-  ( ( P e. Word V /\ ( ( # ` P ) - 1 ) e. ( 0 ... ( # ` P ) ) ) -> ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) = ( ( # ` P ) - 1 ) )
12 10 11 syldan 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) = ( ( # ` P ) - 1 ) )
13 8 nn0cnd 
 |-  ( P e. Word V -> ( # ` P ) e. CC )
14 1cnd 
 |-  ( P e. Word V -> 1 e. CC )
15 13 14 subcld 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) e. CC )
16 15 subid1d 
 |-  ( P e. Word V -> ( ( ( # ` P ) - 1 ) - 0 ) = ( ( # ` P ) - 1 ) )
17 16 eqcomd 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( ( # ` P ) - 1 ) - 0 ) )
18 17 adantr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) = ( ( ( # ` P ) - 1 ) - 0 ) )
19 12 18 eqtrd 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) = ( ( ( # ` P ) - 1 ) - 0 ) )
20 19 oveq1d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) = ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) )
21 20 oveq2d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) = ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
22 12 oveq1d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) = ( ( ( # ` P ) - 1 ) - 1 ) )
23 22 oveq2d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) = ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) )
24 23 eleq2d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) <-> i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) )
25 simpll 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> P e. Word V )
26 wrdlenge2n0 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> P =/= (/) )
27 26 adantr 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> P =/= (/) )
28 nn0z 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
29 peano2zm 
 |-  ( ( # ` P ) e. ZZ -> ( ( # ` P ) - 1 ) e. ZZ )
30 28 29 syl 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. ZZ )
31 8 30 syl 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) e. ZZ )
32 31 adantr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. ZZ )
33 elfzom1elfzo 
 |-  ( ( ( ( # ` P ) - 1 ) e. ZZ /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
34 32 33 sylan 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
35 pfxtrcfv 
 |-  ( ( P e. Word V /\ P =/= (/) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) = ( P ` i ) )
36 25 27 34 35 syl3anc 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) = ( P ` i ) )
37 8 adantr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. NN0 )
38 elfzom1elp1fzo 
 |-  ( ( ( ( # ` P ) - 1 ) e. ZZ /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
39 30 38 sylan 
 |-  ( ( ( # ` P ) e. NN0 /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
40 37 39 sylan 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
41 pfxtrcfv 
 |-  ( ( P e. Word V /\ P =/= (/) /\ ( i + 1 ) e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
42 25 27 40 41 syl3anc 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
43 36 42 preq12d 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
44 43 eleq1d 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) ) -> ( { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
45 44 ex 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( i e. ( 0 ..^ ( ( ( # ` P ) - 1 ) - 1 ) ) -> ( { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) ) )
46 24 45 sylbid 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) -> ( { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) ) )
47 46 imp 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) ) -> ( { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
48 21 47 raleqbidva 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E <-> A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
49 pfxtrcfvl 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) = ( P ` ( ( # ` P ) - 2 ) ) )
50 pfxtrcfv0 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) = ( P ` 0 ) )
51 49 50 preq12d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } )
52 51 eleq1d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E <-> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) )
53 48 52 anbi12d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) <-> ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) )
54 53 bicomd 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( 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 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) )
55 54 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( 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 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) )
56 pfxcl 
 |-  ( P e. Word V -> ( P prefix ( ( # ` P ) - 1 ) ) e. Word V )
57 56 3ad2ant2 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P prefix ( ( # ` P ) - 1 ) ) e. Word V )
58 57 3biant1d 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) )
59 55 58 bitrd 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) )
60 59 anbi2d 
 |-  ( ( G e. USPGraph /\ 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 ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) ) )
61 7 60 bitrd 
 |-  ( ( G e. USPGraph /\ 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 ) /\ ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) ) )
62 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
63 1 2 isclwlkupgr 
 |-  ( G e. UPGraph -> ( f ( ClWalks ` G ) 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 ) ) ) ) ) )
64 3an4anass 
 |-  ( ( ( 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 /\ P : ( 0 ... ( # ` f ) ) --> V ) /\ ( A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) )
65 63 64 bitr4di 
 |-  ( G e. UPGraph -> ( f ( ClWalks ` G ) 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 ) ) ) ) )
66 62 65 syl 
 |-  ( G e. USPGraph -> ( f ( ClWalks ` G ) 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 ) ) ) ) )
67 66 adantr 
 |-  ( ( G e. USPGraph /\ P e. Word V ) -> ( f ( ClWalks ` G ) 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 ) ) ) ) )
68 67 exbidv 
 |-  ( ( G e. USPGraph /\ P e. Word V ) -> ( E. f f ( ClWalks ` G ) 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 ) ) ) ) )
69 68 3adant3 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f f ( ClWalks ` G ) 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 ) ) ) ) )
70 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
71 1 70 isclwwlk 
 |-  ( ( P prefix ( ( # ` P ) - 1 ) ) e. ( ClWWalks ` G ) <-> ( ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ ( P prefix ( ( # ` P ) - 1 ) ) =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ( Edg ` G ) ) )
72 simpl 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> P e. Word V )
73 nn0ge2m1nn 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. NN )
74 8 73 sylan 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. NN )
75 nn0re 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
76 75 lem1d 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) <_ ( # ` P ) )
77 76 a1d 
 |-  ( ( # ` P ) e. NN0 -> ( 2 <_ ( # ` P ) -> ( ( # ` P ) - 1 ) <_ ( # ` P ) ) )
78 8 77 syl 
 |-  ( P e. Word V -> ( 2 <_ ( # ` P ) -> ( ( # ` P ) - 1 ) <_ ( # ` P ) ) )
79 78 imp 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) <_ ( # ` P ) )
80 72 74 79 3jca 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN /\ ( ( # ` P ) - 1 ) <_ ( # ` P ) ) )
81 80 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN /\ ( ( # ` P ) - 1 ) <_ ( # ` P ) ) )
82 pfxn0 
 |-  ( ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN /\ ( ( # ` P ) - 1 ) <_ ( # ` P ) ) -> ( P prefix ( ( # ` P ) - 1 ) ) =/= (/) )
83 81 82 syl 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P prefix ( ( # ` P ) - 1 ) ) =/= (/) )
84 83 biantrud 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ ( P prefix ( ( # ` P ) - 1 ) ) =/= (/) ) ) )
85 84 bicomd 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ ( P prefix ( ( # ` P ) - 1 ) ) =/= (/) ) <-> ( P prefix ( ( # ` P ) - 1 ) ) e. Word V ) )
86 85 3anbi1d 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ ( P prefix ( ( # ` P ) - 1 ) ) =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ( Edg ` G ) ) <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ( Edg ` G ) ) ) )
87 71 86 bitrid 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) e. ( ClWWalks ` G ) <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ( Edg ` G ) ) ) )
88 biid 
 |-  ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V <-> ( P prefix ( ( # ` P ) - 1 ) ) e. Word V )
89 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
90 2 eqcomi 
 |-  ( iEdg ` G ) = E
91 90 rneqi 
 |-  ran ( iEdg ` G ) = ran E
92 89 91 eqtri 
 |-  ( Edg ` G ) = ran E
93 92 eleq2i 
 |-  ( { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E )
94 93 ralbii 
 |-  ( A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E )
95 92 eleq2i 
 |-  ( { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ( Edg ` G ) <-> { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E )
96 88 94 95 3anbi123i 
 |-  ( ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ( Edg ` G ) ) <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) )
97 87 96 bitrdi 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( P prefix ( ( # ` P ) - 1 ) ) e. ( ClWWalks ` G ) <-> ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) )
98 97 anbi2d 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( P prefix ( ( # ` P ) - 1 ) ) e. ( ClWWalks ` G ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( ( P prefix ( ( # ` P ) - 1 ) ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( P prefix ( ( # ` P ) - 1 ) ) ) - 1 ) ) { ( ( P prefix ( ( # ` P ) - 1 ) ) ` i ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` ( P prefix ( ( # ` P ) - 1 ) ) ) , ( ( P prefix ( ( # ` P ) - 1 ) ) ` 0 ) } e. ran E ) ) ) )
99 61 69 98 3bitr4d 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f f ( ClWalks ` G ) P <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( P prefix ( ( # ` P ) - 1 ) ) e. ( ClWWalks ` G ) ) ) )