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

Metamath Proof Explorer

Theorem upgredginwlk

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)

Ref Expression
Hypotheses edginwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
edginwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion upgredginwlk ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼 ) → ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 edginwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 edginwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
4 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
5 3 4 syl ⊢ ( 𝐺 ∈ UPGraph → Fun 𝐼 )
6 1 2 edginwlk ⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 )
7 6 3expia ⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ) → ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 ) )
8 5 7 sylan ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼 ) → ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 ) )