Theorem edginwlk

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) (Revised by AV, 9-Dec-2021)

	Ref	Expression
Hypotheses	edginwlk.i	|- I = ( iEdg ` G )
	edginwlk.e	|- E = ( Edg ` G )
Assertion	edginwlk	|- ( ( Fun I /\ 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		simp1	|- ( ( Fun I /\ F e. Word dom I /\ K e. ( 0 ..^ ( # ` F ) ) ) -> Fun I )
4		wrdsymbcl	|- ( ( F e. Word dom I /\ K e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` K ) e. dom I )
5	4	3adant1	|- ( ( Fun I /\ F e. Word dom I /\ K e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` K ) e. dom I )
6		fvelrn	|- ( ( Fun I /\ ( F ` K ) e. dom I ) -> ( I ` ( F ` K ) ) e. ran I )
7	3 5 6	syl2anc	|- ( ( Fun I /\ F e. Word dom I /\ K e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` K ) ) e. ran I )
8		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
9	1	eqcomi	|- ( iEdg ` G ) = I
10	9	rneqi	|- ran ( iEdg ` G ) = ran I
11	2 8 10	3eqtri	|- E = ran I
12	7 11	eleqtrrdi	|- ( ( Fun I /\ F e. Word dom I /\ K e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` K ) ) e. E )