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