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=\mathrm{Vtx}\left(G\right)$$
Assertion	0pthonv	$$⊢N\in V\to \exists f\exists pf\left(N\mathrm{PathsOn}\left(G\right)N\right)p$$

Proof

Step	Hyp	Ref	Expression
1		0pthon.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		snex	$$⊢\left\{⟨0,N⟩\right\}\in \mathrm{V}$$
4	2 3	pm3.2i	$$⊢\left(\varnothing \in \mathrm{V}\wedge \left\{⟨0,N⟩\right\}\in \mathrm{V}\right)$$
5	1	0pthon1	$$⊢N\in V\to \varnothing \left(N\mathrm{PathsOn}\left(G\right)N\right)\left\{⟨0,N⟩\right\}$$
6		breq12	$$⊢\left(f=\varnothing \wedge p=\left\{⟨0,N⟩\right\}\right)\to \left(f\left(N\mathrm{PathsOn}\left(G\right)N\right)p\leftrightarrow \varnothing \left(N\mathrm{PathsOn}\left(G\right)N\right)\left\{⟨0,N⟩\right\}\right)$$
7	6	spc2egv	$$⊢\left(\varnothing \in \mathrm{V}\wedge \left\{⟨0,N⟩\right\}\in \mathrm{V}\right)\to \left(\varnothing \left(N\mathrm{PathsOn}\left(G\right)N\right)\left\{⟨0,N⟩\right\}\to \exists f\exists pf\left(N\mathrm{PathsOn}\left(G\right)N\right)p\right)$$
8	4 5 7	mpsyl	$$⊢N\in V\to \exists f\exists pf\left(N\mathrm{PathsOn}\left(G\right)N\right)p$$