Metamath Proof Explorer

Theorem 0pthon1

Description: A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 20-Jan-2021)

Ref Expression
Hypothesis 0pthon.v 
|- V = ( Vtx ` G )
Assertion 0pthon1 
|- ( N e. V -> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } )

Proof

Step Hyp Ref Expression
1 0pthon.v 
 |-  V = ( Vtx ` G )
2 eqidd 
 |-  ( N e. V -> { <. 0 , N >. } = { <. 0 , N >. } )
3 1fv 
 |-  ( ( N e. V /\ { <. 0 , N >. } = { <. 0 , N >. } ) -> ( { <. 0 , N >. } : ( 0 ... 0 ) --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) )
4 2 3 mpdan 
 |-  ( N e. V -> ( { <. 0 , N >. } : ( 0 ... 0 ) --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) )
5 1 0pthon 
 |-  ( ( { <. 0 , N >. } : ( 0 ... 0 ) --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) -> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } )
6 4 5 syl 
 |-  ( N e. V -> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } )