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

Metamath Proof Explorer

Theorem upgredginwlk

Description: The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021)

Ref Expression
Hypotheses edginwlk.i 
|- I = ( iEdg ` G )
edginwlk.e 
|- E = ( Edg ` G )
Assertion upgredginwlk 
|- ( ( G e. UPGraph /\ F e. Word dom I ) -> ( K e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` K ) ) e. E ) )

Proof

Step Hyp Ref Expression
1 edginwlk.i 
 |-  I = ( iEdg ` G )
2 edginwlk.e 
 |-  E = ( Edg ` G )
3 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
4 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
5 3 4 syl 
 |-  ( G e. UPGraph -> Fun I )
6 1 2 edginwlk 
 |-  ( ( Fun I /\ F e. Word dom I /\ K e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` K ) ) e. E )
7 6 3expia 
 |-  ( ( Fun I /\ F e. Word dom I ) -> ( K e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` K ) ) e. E ) )
8 5 7 sylan 
 |-  ( ( G e. UPGraph /\ F e. Word dom I ) -> ( K e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` K ) ) e. E ) )