Metamath Proof Explorer

Theorem wlkepvtx

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

Ref Expression
Hypothesis wlkpvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wlkepvtx ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 wlkpvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
3 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
4 0elfz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
5 ffvelrn ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
6 4 5 sylan2 ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
7 nn0fz0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
8 ffvelrn ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ 𝑉 )
9 7 8 sylan2b ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ 𝑉 )
10 6 9 jca ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ 𝑉 ) )
11 2 3 10 syl2anc ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ 𝑉 ) )