Theorem is0wlk

Description: A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypothesis	0wlk.v	|- V = ( Vtx ` G )
Assertion	is0wlk	|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> (/) ( Walks ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	|- V = ( Vtx ` G )
2		1fv	|- ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) )
3	2	ancoms	|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) )
4	3	simpld	|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> P : ( 0 ... 0 ) --> V )
5	1	1vgrex	|- ( N e. V -> G e. _V )
6	5	adantl	|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> G e. _V )
7	1	0wlk	|- ( G e. _V -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
8	6 7	syl	|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
9	4 8	mpbird	|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> (/) ( Walks ` G ) P )