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

Metamath Proof Explorer

Theorem wlkf

Description: The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021)

Ref Expression
Hypothesis wlkf.i ⊢ I = iEdg ⁡ G
Assertion wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I

Proof

Step Hyp Ref Expression
1 wlkf.i ⊢ I = iEdg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 1 wlkprop ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
4 3 simp1d ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I