Metamath Proof Explorer

Theorem wlkonwlk

Description: A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 31-Jan-2021)

Ref Expression
Assertion wlkonwlk ⊢ F Walks ⁡ G P → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P

Proof

Step Hyp Ref Expression
1 id ⊢ F Walks ⁡ G P → F Walks ⁡ G P
2 eqidd ⊢ F Walks ⁡ G P → P ⁡ 0 = P ⁡ 0
3 eqidd ⊢ F Walks ⁡ G P → P ⁡ F = P ⁡ F
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 wlkepvtx ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G
6 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
7 3simpc ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ V ∧ P ∈ V
8 6 7 syl ⊢ F Walks ⁡ G P → F ∈ V ∧ P ∈ V
9 4 iswlkon ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ 0 ∧ P ⁡ F = P ⁡ F
10 5 8 9 syl2anc ⊢ F Walks ⁡ G P → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ 0 ∧ P ⁡ F = P ⁡ F
11 1 2 3 10 mpbir3and ⊢ F Walks ⁡ G P → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P