Metamath Proof Explorer

Theorem wlkprop

Description: Properties of a walk. (Contributed by AV, 5-Nov-2021)

Ref Expression
Hypotheses wksfval.v ⊢ V = Vtx ⁡ G
wksfval.i ⊢ I = iEdg ⁡ G
Assertion wlkprop ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 wksfval.v ⊢ V = Vtx ⁡ G
2 wksfval.i ⊢ I = iEdg ⁡ G
3 1 2 wksfval ⊢ G ∈ V → Walks ⁡ G = f p | f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 I ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ I ⁡ f ⁡ k
4 3 brfvopab ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
5 1 2 iswlk ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
6 5 biimpd ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
7 4 6 mpcom ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k