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

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 )