Metamath Proof Explorer

Theorem wlkvtxeledg

Description: Each pair of adjacent vertices in a walk is a subset of an edge. (Contributed by AV, 28-Jan-2021) (Proof shortened by AV, 4-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 wlkvtxeledg.i ⊢ I = iEdg ⁡ G
2 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 1 iswlk ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → 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
5 ifpsnprss ⊢ if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
6 5 ralimi ⊢ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
7 6 3ad2ant3 ⊢ 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 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
8 4 7 biimtrdi ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
9 2 8 mpcom ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k