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	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	iedginwlk	⊢ ( ( Fun 𝐼 ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		iedginwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		simp1	⊢ ( ( Fun 𝐼 ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun 𝐼 )
3	1	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
4	3	3ad2ant2	⊢ ( ( Fun 𝐼 ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ Word dom 𝐼 )
5		simp3	⊢ ( ( Fun 𝐼 ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6		wrdsymbcl	⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 )
7	4 5 6	syl2anc	⊢ ( ( Fun 𝐼 ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 )
8		fvelrn	⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ran 𝐼 )
9	2 7 8	syl2anc	⊢ ( ( Fun 𝐼 ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ran 𝐼 )