This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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