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 e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` X ) ) e. ran I )

Proof

Step Hyp Ref Expression
1 iedginwlk.i 
 |-  I = ( iEdg ` G )
2 simp1 
 |-  ( ( Fun I /\ F ( Walks ` G ) P /\ X e. ( 0 ..^ ( # ` F ) ) ) -> Fun I )
3 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
4 3 3ad2ant2 
 |-  ( ( Fun I /\ F ( Walks ` G ) P /\ X e. ( 0 ..^ ( # ` F ) ) ) -> F e. Word dom I )
5 simp3 
 |-  ( ( Fun I /\ F ( Walks ` G ) P /\ X e. ( 0 ..^ ( # ` F ) ) ) -> X e. ( 0 ..^ ( # ` F ) ) )
6 wrdsymbcl 
 |-  ( ( F e. Word dom I /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` X ) e. dom I )
7 4 5 6 syl2anc 
 |-  ( ( Fun I /\ F ( Walks ` G ) P /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` X ) e. dom I )
8 fvelrn 
 |-  ( ( Fun I /\ ( F ` X ) e. dom I ) -> ( I ` ( F ` X ) ) e. ran I )
9 2 7 8 syl2anc 
 |-  ( ( Fun I /\ F ( Walks ` G ) P /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` X ) ) e. ran I )