Metamath Proof Explorer


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 Word dom I K 0 ..^ F I F K E

Proof

Step Hyp Ref Expression
1 edginwlk.i I = iEdg G
2 edginwlk.e E = Edg G
3 simp1 Fun I F Word dom I K 0 ..^ F Fun I
4 wrdsymbcl F Word dom I K 0 ..^ F F K dom I
5 4 3adant1 Fun I F Word dom I K 0 ..^ F F K dom I
6 fvelrn Fun I F K dom I I F K ran I
7 3 5 6 syl2anc Fun I F Word dom I K 0 ..^ F I F K 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 Word dom I K 0 ..^ F I F K E