This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$

Proof

Step	Hyp	Ref	Expression
1		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
4		ffz0hash	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to \|P\| = \|F\| + 1$
5	1 3 4	syl2anc	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$