This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkn0

Description: The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlkn0 
|- ( F ( Walks ` G ) P -> P =/= (/) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
3 fdm 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> dom P = ( 0 ... ( # ` F ) ) )
4 3 eqcomd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( 0 ... ( # ` F ) ) = dom P )
5 2 4 syl 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` F ) ) = dom P )
6 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
7 elnn0uz 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( ZZ>= ` 0 ) )
8 fzn0 
 |-  ( ( 0 ... ( # ` F ) ) =/= (/) <-> ( # ` F ) e. ( ZZ>= ` 0 ) )
9 7 8 sylbb2 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ... ( # ` F ) ) =/= (/) )
10 6 9 syl 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` F ) ) =/= (/) )
11 5 10 eqnetrrd 
 |-  ( F ( Walks ` G ) P -> dom P =/= (/) )
12 frel 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> Rel P )
13 2 12 syl 
 |-  ( F ( Walks ` G ) P -> Rel P )
14 reldm0 
 |-  ( Rel P -> ( P = (/) <-> dom P = (/) ) )
15 14 necon3bid 
 |-  ( Rel P -> ( P =/= (/) <-> dom P =/= (/) ) )
16 13 15 syl 
 |-  ( F ( Walks ` G ) P -> ( P =/= (/) <-> dom P =/= (/) ) )
17 11 16 mpbird 
 |-  ( F ( Walks ` G ) P -> P =/= (/) )