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