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

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 )