Metamath Proof Explorer


Theorem 0pthonv

Description: For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 21-Jan-2021)

Ref Expression
Hypothesis 0pthon.v
|- V = ( Vtx ` G )
Assertion 0pthonv
|- ( N e. V -> E. f E. p f ( N ( PathsOn ` G ) N ) p )

Proof

Step Hyp Ref Expression
1 0pthon.v
 |-  V = ( Vtx ` G )
2 0ex
 |-  (/) e. _V
3 snex
 |-  { <. 0 , N >. } e. _V
4 2 3 pm3.2i
 |-  ( (/) e. _V /\ { <. 0 , N >. } e. _V )
5 1 0pthon1
 |-  ( N e. V -> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } )
6 breq12
 |-  ( ( f = (/) /\ p = { <. 0 , N >. } ) -> ( f ( N ( PathsOn ` G ) N ) p <-> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } ) )
7 6 spc2egv
 |-  ( ( (/) e. _V /\ { <. 0 , N >. } e. _V ) -> ( (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } -> E. f E. p f ( N ( PathsOn ` G ) N ) p ) )
8 4 5 7 mpsyl
 |-  ( N e. V -> E. f E. p f ( N ( PathsOn ` G ) N ) p )