Metamath Proof Explorer

Theorem wlkiswwlksupgr2

Description: A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of wlkiswwlks2 does not require G to be a simple pseudograph, but it requires the Axiom of Choice ( ac6 ) for its proof. Notice that only the existence of a function f can be proven, but, in general, it cannot be "constructed" (as in wlkiswwlks2 ). (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 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 ) ) )
4 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
5 4 eleq2i 
 |-  ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) )
6 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
7 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
8 7 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
9 6 8 syl 
 |-  ( G e. UPGraph -> Fun ( iEdg ` G ) )
10 9 adantl 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ G e. UPGraph ) -> Fun ( iEdg ` G ) )
11 elrnrexdm 
 |-  ( Fun ( iEdg ` G ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) -> E. x e. dom ( iEdg ` G ) { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( ( iEdg ` G ) ` x ) ) )
12 eqcom 
 |-  ( ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( ( iEdg ` G ) ` x ) )
13 12 rexbii 
 |-  ( E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> E. x e. dom ( iEdg ` G ) { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( ( iEdg ` G ) ` x ) )
14 11 13 syl6ibr 
 |-  ( Fun ( iEdg ` G ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) -> E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
15 10 14 syl 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ G e. UPGraph ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran ( iEdg ` G ) -> E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
16 5 15 syl5bi 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ G e. UPGraph ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
17 16 ralimdv 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ G e. UPGraph ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
18 17 ex 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( G e. UPGraph -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
19 18 com23 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( G e. UPGraph -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
20 19 3impia 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( G e. UPGraph -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
21 20 impcom 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
22 ovex 
 |-  ( 0 ..^ ( ( # ` P ) - 1 ) ) e. _V
23 fvex 
 |-  ( iEdg ` G ) e. _V
24 23 dmex 
 |-  dom ( iEdg ` G ) e. _V
25 fveqeq2 
 |-  ( x = ( f ` i ) -> ( ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
26 22 24 25 ac6 
 |-  ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) E. x e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` x ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> E. f ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
27 21 26 syl 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> E. f ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
28 iswrdi 
 |-  ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> f e. Word dom ( iEdg ` G ) )
29 28 adantr 
 |-  ( ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> f e. Word dom ( iEdg ` G ) )
30 29 adantl 
 |-  ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> f e. Word dom ( iEdg ` G ) )
31 len0nnbi 
 |-  ( P e. Word ( Vtx ` G ) -> ( P =/= (/) <-> ( # ` P ) e. NN ) )
32 31 biimpac 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( # ` P ) e. NN )
33 wrdf 
 |-  ( P e. Word ( Vtx ` G ) -> P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) )
34 nnz 
 |-  ( ( # ` P ) e. NN -> ( # ` P ) e. ZZ )
35 fzoval 
 |-  ( ( # ` P ) e. ZZ -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
36 34 35 syl 
 |-  ( ( # ` P ) e. NN -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
37 36 adantr 
 |-  ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
38 nnm1nn0 
 |-  ( ( # ` P ) e. NN -> ( ( # ` P ) - 1 ) e. NN0 )
39 fnfzo0hash 
 |-  ( ( ( ( # ` P ) - 1 ) e. NN0 /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( # ` f ) = ( ( # ` P ) - 1 ) )
40 38 39 sylan 
 |-  ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( # ` f ) = ( ( # ` P ) - 1 ) )
41 40 eqcomd 
 |-  ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( ( # ` P ) - 1 ) = ( # ` f ) )
42 41 oveq2d 
 |-  ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` f ) ) )
43 37 42 eqtrd 
 |-  ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` f ) ) )
44 43 feq2d 
 |-  ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) <-> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
45 44 biimpcd 
 |-  ( P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) -> ( ( ( # ` P ) e. NN /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
46 45 expd 
 |-  ( P : ( 0 ..^ ( # ` P ) ) --> ( Vtx ` G ) -> ( ( # ` P ) e. NN -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) ) )
47 33 46 syl 
 |-  ( P e. Word ( Vtx ` G ) -> ( ( # ` P ) e. NN -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) ) )
48 47 adantl 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( ( # ` P ) e. NN -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) ) )
49 32 48 mpd 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
50 49 3adant3 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
51 50 adantl 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
52 51 com12 
 |-  ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
53 52 adantr 
 |-  ( ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) ) )
54 53 impcom 
 |-  ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> P : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) )
55 simpr 
 |-  ( ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
56 32 40 sylan 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( # ` f ) = ( ( # ` P ) - 1 ) )
57 56 oveq2d 
 |-  ( ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) )
58 57 ex 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) ) -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) ) )
59 58 3adant3 
 |-  ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) ) )
60 59 adantl 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) ) )
61 60 imp 
 |-  ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) )
62 61 adantr 
 |-  ( ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) )
63 62 raleqdv 
 |-  ( ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
64 55 63 mpbird 
 |-  ( ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
65 64 anasss 
 |-  ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> A. i e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
66 30 54 65 3jca 
 |-  ( ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 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 ) ) } ) )
67 66 ex 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 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 ) ) } ) ) )
68 67 eximdv 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( E. f ( f : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( ( iEdg ` G ) ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> 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 ) ) } ) ) )
69 27 68 mpd 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ 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 ) ) } ) )
70 1 7 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 ) ) } ) ) )
71 70 adantr 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( 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 ) ) } ) ) )
72 71 exbidv 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( 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 ) ) } ) ) )
73 69 72 mpbird 
 |-  ( ( G e. UPGraph /\ ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> E. f f ( Walks ` G ) P )
74 73 ex 
 |-  ( G e. UPGraph -> ( ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> E. f f ( Walks ` G ) P ) )
75 3 74 syl5bi 
 |-  ( G e. UPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )