Metamath Proof Explorer


Theorem iedginwlk

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

Ref Expression
Hypothesis iedginwlk.i I = iEdg G
Assertion iedginwlk Fun I F Walks G P X 0 ..^ F I F X ran I

Proof

Step Hyp Ref Expression
1 iedginwlk.i I = iEdg G
2 simp1 Fun I F Walks G P X 0 ..^ F Fun I
3 1 wlkf F Walks G P F Word dom I
4 3 3ad2ant2 Fun I F Walks G P X 0 ..^ F F Word dom I
5 simp3 Fun I F Walks G P X 0 ..^ F X 0 ..^ F
6 wrdsymbcl F Word dom I X 0 ..^ F F X dom I
7 4 5 6 syl2anc Fun I F Walks G P X 0 ..^ F F X dom I
8 fvelrn Fun I F X dom I I F X ran I
9 2 7 8 syl2anc Fun I F Walks G P X 0 ..^ F I F X ran I