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 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 ) )