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 ) e. V /\ ( P ` ( # ` F ) ) 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 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
4 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
5 ffvelrn 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ 0 e. ( 0 ... ( # ` F ) ) ) -> ( P ` 0 ) e. V )
6 4 5 sylan2 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( # ` F ) e. NN0 ) -> ( P ` 0 ) e. V )
7 nn0fz0 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
8 ffvelrn 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) ) -> ( P ` ( # ` F ) ) e. V )
9 7 8 sylan2b 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( # ` F ) e. NN0 ) -> ( P ` ( # ` F ) ) e. V )
10 6 9 jca 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( # ` F ) e. NN0 ) -> ( ( P ` 0 ) e. V /\ ( P ` ( # ` F ) ) e. V ) )
11 2 3 10 syl2anc 
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) e. V /\ ( P ` ( # ` F ) ) e. V ) )