Metamath Proof Explorer

Theorem wwlkbp

Description: Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Hypothesis wwlkbp.v ⊢ V = Vtx ⁡ G
Assertion wwlkbp ⊢ W ∈ WWalks ⁡ G → G ∈ V ∧ W ∈ Word V

Proof

Step Hyp Ref Expression
1 wwlkbp.v ⊢ V = Vtx ⁡ G
2 elfvex ⊢ W ∈ WWalks ⁡ G → G ∈ V
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 iswwlks ⊢ W ∈ WWalks ⁡ G ↔ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
5 4 simp2bi ⊢ W ∈ WWalks ⁡ G → W ∈ Word V
6 2 5 jca ⊢ W ∈ WWalks ⁡ G → G ∈ V ∧ W ∈ Word V