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 )