Metamath Proof Explorer

Theorem upgrwlkedg

Description: The edges of a walk in a pseudograph join exactly the two corresponding adjacent vertices in the walk. (Contributed by AV, 27-Feb-2021)

Ref Expression
Hypothesis upgrwlkedg.i ⊢ I = iEdg ⁡ G
Assertion upgrwlkedg ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 upgrwlkedg.i ⊢ I = iEdg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 1 upgriswlk ⊢ G ∈ UPGraph → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
4 simp3 ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
5 3 4 biimtrdi ⊢ G ∈ UPGraph → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
6 5 imp ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1