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 ) )