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=\mathrm{Vtx}\left(G\right)$$
Assertion	0pthon1	$$⊢N\in V\to \varnothing \left(N\mathrm{PathsOn}\left(G\right)N\right)\left\{⟨0,N⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		0pthon.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eqidd	$$⊢N\in V\to \left\{⟨0,N⟩\right\}=\left\{⟨0,N⟩\right\}$$
3		1fv	$$⊢\left(N\in V\wedge \left\{⟨0,N⟩\right\}=\left\{⟨0,N⟩\right\}\right)\to \left(\left\{⟨0,N⟩\right\}:\left(0\dots 0\right)⟶V\wedge \left\{⟨0,N⟩\right\}\left(0\right)=N\right)$$
4	2 3	mpdan	$$⊢N\in V\to \left(\left\{⟨0,N⟩\right\}:\left(0\dots 0\right)⟶V\wedge \left\{⟨0,N⟩\right\}\left(0\right)=N\right)$$
5	1	0pthon	$$⊢\left(\left\{⟨0,N⟩\right\}:\left(0\dots 0\right)⟶V\wedge \left\{⟨0,N⟩\right\}\left(0\right)=N\right)\to \varnothing \left(N\mathrm{PathsOn}\left(G\right)N\right)\left\{⟨0,N⟩\right\}$$
6	4 5	syl	$$⊢N\in V\to \varnothing \left(N\mathrm{PathsOn}\left(G\right)N\right)\left\{⟨0,N⟩\right\}$$