Metamath Proof Explorer

Theorem upgrwlkupwlk

Description: In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 2-Jan-2021)

Ref Expression
Assertion upgrwlkupwlk 
|- ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> F ( UPWalks ` G ) P )

Proof

Step Hyp Ref Expression
1 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 2 3 iswlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
5 simpr1 
 |-  ( ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> F e. Word dom ( iEdg ` G ) )
6 simpr2 
 |-  ( ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
7 df-ifp 
 |-  ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } ) \/ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
8 dfsn2 
 |-  { ( P ` k ) } = { ( P ` k ) , ( P ` k ) }
9 preq2 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> { ( P ` k ) , ( P ` k ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
10 8 9 syl5eq 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> { ( P ` k ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
11 10 eqeq2d 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } <-> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
12 11 biimpa 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
13 12 a1d 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } ) -> ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
14 simpr 
 |-  ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) -> G e. UPGraph )
15 simpl 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> F e. Word dom ( iEdg ` G ) )
16 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
17 3 16 upgredginwlk 
 |-  ( ( G e. UPGraph /\ F e. Word dom ( iEdg ` G ) ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) )
18 14 15 17 syl2anr 
 |-  ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) )
19 18 imp 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) )
20 simprr 
 |-  ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) -> G e. UPGraph )
21 20 adantr 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> G e. UPGraph )
22 21 adantr 
 |-  ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) -> G e. UPGraph )
23 22 adantr 
 |-  ( ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> G e. UPGraph )
24 simplr 
 |-  ( ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) )
25 simprr 
 |-  ( ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) )
26 df-ne 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) <-> -. ( P ` k ) = ( P ` ( k + 1 ) ) )
27 fvexd 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( P ` k ) e. _V )
28 fvexd 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( P ` ( k + 1 ) ) e. _V )
29 id 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) )
30 27 28 29 3jca 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
31 26 30 sylbir 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
32 31 adantr 
 |-  ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
33 32 adantl 
 |-  ( ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
34 2 16 upgredgpr 
 |-  ( ( ( G e. UPGraph /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) /\ ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = ( ( iEdg ` G ) ` ( F ` k ) ) )
35 23 24 25 33 34 syl31anc 
 |-  ( ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = ( ( iEdg ` G ) ` ( F ` k ) ) )
36 35 eqcomd 
 |-  ( ( ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
37 36 exp31 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` k ) ) e. ( Edg ` G ) -> ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
38 19 37 mpd 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
39 38 com12 
 |-  ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
40 13 39 jaoi 
 |-  ( ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } ) \/ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
41 40 com12 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } ) \/ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
42 7 41 syl5bi 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
43 42 ralimdva 
 |-  ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
44 43 ex 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
45 44 com23 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
46 45 3impia 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
47 46 impcom 
 |-  ( ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
48 5 6 47 3jca 
 |-  ( ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ G e. UPGraph ) /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
49 48 exp31 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( G e. UPGraph -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) )
50 49 com23 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( G e. UPGraph -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) )
51 4 50 sylbid 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P -> ( G e. UPGraph -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) )
52 51 impd 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( ( F ( Walks ` G ) P /\ G e. UPGraph ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
53 52 impcom 
 |-  ( ( ( F ( Walks ` G ) P /\ G e. UPGraph ) /\ ( G e. _V /\ F e. _V /\ P e. _V ) ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
54 2 3 isupwlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
55 54 adantl 
 |-  ( ( ( F ( Walks ` G ) P /\ G e. UPGraph ) /\ ( G e. _V /\ F e. _V /\ P e. _V ) ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
56 53 55 mpbird 
 |-  ( ( ( F ( Walks ` G ) P /\ G e. UPGraph ) /\ ( G e. _V /\ F e. _V /\ P e. _V ) ) -> F ( UPWalks ` G ) P )
57 56 exp31 
 |-  ( F ( Walks ` G ) P -> ( G e. UPGraph -> ( ( G e. _V /\ F e. _V /\ P e. _V ) -> F ( UPWalks ` G ) P ) ) )
58 1 57 mpid 
 |-  ( F ( Walks ` G ) P -> ( G e. UPGraph -> F ( UPWalks ` G ) P ) )
59 58 impcom 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> F ( UPWalks ` G ) P )