Metamath Proof Explorer

Theorem wlkiswwlks2

Description: A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Assertion wlkiswwlks2 
|- ( G e. USPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wwlkbp 
 |-  ( P e. ( WWalks ` G ) -> ( G e. _V /\ P e. Word ( Vtx ` G ) ) )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 1 3 iswwlks 
 |-  ( P e. ( WWalks ` G ) <-> ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
5 ovex 
 |-  ( 0 ..^ ( ( # ` P ) - 1 ) ) e. _V
6 mptexg 
 |-  ( ( 0 ..^ ( ( # ` P ) - 1 ) ) e. _V -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. _V )
7 5 6 mp1i 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. _V )
8 simprr 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) -> G e. USPGraph )
9 simplr 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) -> P e. Word ( Vtx ` G ) )
10 hashge1 
 |-  ( ( P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> 1 <_ ( # ` P ) )
11 10 ancoms 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> 1 <_ ( # ` P ) )
12 11 adantr 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) -> 1 <_ ( # ` P ) )
13 8 9 12 3jca 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) -> ( G e. USPGraph /\ P e. Word ( Vtx ` G ) /\ 1 <_ ( # ` P ) ) )
14 13 adantr 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( G e. USPGraph /\ P e. Word ( Vtx ` G ) /\ 1 <_ ( # ` P ) ) )
15 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
16 15 a1i 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( Edg ` G ) = ran ( iEdg ` G ) )
17 16 eleq2d 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) ) )
18 17 ralbidv 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) ) )
19 18 biimpd 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) ) )
20 eqid 
 |-  ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
21 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
22 20 21 wlkiswwlks2lem6 
 |-  ( ( G e. USPGraph /\ P e. Word ( Vtx ` G ) /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
23 14 19 22 sylsyld 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
24 eleq1 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( f e. Word dom ( iEdg ` G ) <-> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. Word dom ( iEdg ` G ) ) )
25 fveq2 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( # ` f ) = ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) )
26 25 oveq2d 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( 0 ... ( # ` f ) ) = ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) )
27 26 feq2d 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) <-> P : ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) --> ( Vtx ` G ) ) )
28 25 oveq2d 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) )
29 fveq1 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( f ` i ) = ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) )
30 29 fveqeq2d 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
31 28 30 raleqbidv 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
32 24 27 31 3anbi123d 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) <-> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
33 32 imbi2d 
 |-  ( f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) <-> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) ) )
34 33 adantl 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) <-> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) ) ( ( iEdg ` G ) ` ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) ) )
35 23 34 mpbird 
 |-  ( ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) /\ f = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' ( iEdg ` G ) ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
36 7 35 spcimedv 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
37 36 ex 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) ) )
38 37 com23 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) ) )
39 38 3impia 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ G e. USPGraph ) -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
40 39 expd 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) -> ( G e. USPGraph -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) ) )
41 40 impcom 
 |-  ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( G e. USPGraph -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
42 41 imp 
 |-  ( ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ G e. USPGraph ) -> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
43 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
44 1 21 upgriswlk 
 |-  ( G e. UPGraph -> ( f ( Walks ` G ) P <-> ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
45 43 44 syl 
 |-  ( G e. USPGraph -> ( f ( Walks ` G ) P <-> ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
46 45 adantl 
 |-  ( ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ G e. USPGraph ) -> ( f ( Walks ` G ) P <-> ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
47 46 exbidv 
 |-  ( ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ G e. USPGraph ) -> ( E. f f ( Walks ` G ) P <-> E. f ( f e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
48 42 47 mpbird 
 |-  ( ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ G e. USPGraph ) -> E. f f ( Walks ` G ) P )
49 48 ex 
 |-  ( ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( G e. USPGraph -> E. f f ( Walks ` G ) P ) )
50 49 ex 
 |-  ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) -> ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( G e. USPGraph -> E. f f ( Walks ` G ) P ) ) )
51 4 50 syl5bi 
 |-  ( ( G e. _V /\ P e. Word ( Vtx ` G ) ) -> ( P e. ( WWalks ` G ) -> ( G e. USPGraph -> E. f f ( Walks ` G ) P ) ) )
52 2 51 mpcom 
 |-  ( P e. ( WWalks ` G ) -> ( G e. USPGraph -> E. f f ( Walks ` G ) P ) )
53 52 com12 
 |-  ( G e. USPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )