Theorem wlkpvtx

Description: A walk connects vertices. (Contributed by AV, 22-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		wlkpvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	wlkp	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
3		ffvelrn	⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 )
4	3	ex	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ) )
5	2 4	syl	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ) )