Metamath Proof Explorer


Theorem wlklenvp1

Description: The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018) (Revised by AV, 1-May-2021)

Ref Expression
Assertion wlklenvp1 FWalksGPP=F+1

Proof

Step Hyp Ref Expression
1 wlkcl FWalksGPF0
2 eqid VtxG=VtxG
3 2 wlkp FWalksGPP:0FVtxG
4 ffz0hash F0P:0FVtxGP=F+1
5 1 3 4 syl2anc FWalksGPP=F+1