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

Metamath Proof Explorer

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