Theorem wlkpvtx

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

	Ref	Expression
Hypothesis	wlkpvtx.v	|- V = ( Vtx ` G )
Assertion	wlkpvtx	|- ( F ( Walks ` G ) P -> ( N e. ( 0 ... ( # ` F ) ) -> ( P ` N ) e. V ) )

Proof

Step	Hyp	Ref	Expression
1		wlkpvtx.v	|- V = ( Vtx ` G )
2	1	wlkp	|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
3		ffvelrn	|- ( ( P : ( 0 ... ( # ` F ) ) --> V /\ N e. ( 0 ... ( # ` F ) ) ) -> ( P ` N ) e. V )
4	3	ex	|- ( P : ( 0 ... ( # ` F ) ) --> V -> ( N e. ( 0 ... ( # ` F ) ) -> ( P ` N ) e. V ) )
5	2 4	syl	|- ( F ( Walks ` G ) P -> ( N e. ( 0 ... ( # ` F ) ) -> ( P ` N ) e. V ) )