Metamath Proof Explorer


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 )