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 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
edginwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion edginwlk ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 edginwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 edginwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 simp1 ⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun 𝐼 )
4 wrdsymbcl ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝐾 ) ∈ dom 𝐼 )
5 4 3adant1 ⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝐾 ) ∈ dom 𝐼 )
6 fvelrn ⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝐾 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ ran 𝐼 )
7 3 5 6 syl2anc ⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ ran 𝐼 )
8 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
9 1 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
10 9 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
11 2 8 10 3eqtri ⊢ 𝐸 = ran 𝐼
12 7 11 eleqtrrdi ⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 )