Metamath Proof Explorer

Theorem 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 → P ⁡ 0 ∈ V ∧ P ⁡ F ∈ V

Proof

Step Hyp Ref Expression
1 wlkpvtx.v ⊢ V = Vtx ⁡ G
2 1 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ V
3 wlkcl ⊢ F Walks ⁡ G P → F ∈ ℕ 0
4 0elfz ⊢ F ∈ ℕ 0 → 0 ∈ 0 … F
5 ffvelrn ⊢ P : 0 … F ⟶ V ∧ 0 ∈ 0 … F → P ⁡ 0 ∈ V
6 4 5 sylan2 ⊢ P : 0 … F ⟶ V ∧ F ∈ ℕ 0 → P ⁡ 0 ∈ V
7 nn0fz0 ⊢ F ∈ ℕ 0 ↔ F ∈ 0 … F
8 ffvelrn ⊢ P : 0 … F ⟶ V ∧ F ∈ 0 … F → P ⁡ F ∈ V
9 7 8 sylan2b ⊢ P : 0 … F ⟶ V ∧ F ∈ ℕ 0 → P ⁡ F ∈ V
10 6 9 jca ⊢ P : 0 … F ⟶ V ∧ F ∈ ℕ 0 → P ⁡ 0 ∈ V ∧ P ⁡ F ∈ V
11 2 3 10 syl2anc ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ V ∧ P ⁡ F ∈ V