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

Metamath Proof Explorer

Theorem wlkp

Description: The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021)

Ref Expression
Hypothesis wlkp.v ⊢ V = Vtx ⁡ G
Assertion wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ V

Proof

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