wlkepvtx

Description: The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021)

		Ref	Expression
	Hypothesis	wlkpvtx.v	$⊢ V = Vtx (G)$
	Assertion	wlkepvtx	$⊢ F Walks (G) P \to (P (0) \in V \land P (\|F\|) \in V)$

Step	Hyp	Ref	Expression
1		wlkpvtx.v	$⊢ V = Vtx (G)$
2	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
3		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
4		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
5		ffvelcdm	$⊢ (P : (0 \dots \|F\|) ⟶ V \land 0 \in (0 \dots \|F\|)) \to P (0) \in V$
6	4 5	sylan2	$⊢ (P : (0 \dots \|F\|) ⟶ V \land \|F\| \in ℕ_{0}) \to P (0) \in V$
7		nn0fz0	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in (0 \dots \|F\|)$
8		ffvelcdm	$⊢ (P : (0 \dots \|F\|) ⟶ V \land \|F\| \in (0 \dots \|F\|)) \to P (\|F\|) \in V$
9	7 8	sylan2b	$⊢ (P : (0 \dots \|F\|) ⟶ V \land \|F\| \in ℕ_{0}) \to P (\|F\|) \in V$
10	6 9	jca	$⊢ (P : (0 \dots \|F\|) ⟶ V \land \|F\| \in ℕ_{0}) \to (P (0) \in V \land P (\|F\|) \in V)$
11	2 3 10	syl2anc	$⊢ F Walks (G) P \to (P (0) \in V \land P (\|F\|) \in V)$

Metamath Proof Explorer