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 =/= (/) )