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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	Assertion	0pthonv	⊢ ( 𝑁 ∈ 𝑉 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		0pthon.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		0ex	⊢ ∅ ∈ V
3		snex	⊢ { ⟨ 0 , 𝑁 ⟩ } ∈ V
4	2 3	pm3.2i	⊢ ( ∅ ∈ V ∧ { ⟨ 0 , 𝑁 ⟩ } ∈ V )
5	1	0pthon1	⊢ ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )
6		breq12	⊢ ( ( 𝑓 = ∅ ∧ 𝑝 = { ⟨ 0 , 𝑁 ⟩ } ) → ( 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 ↔ ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } ) )
7	6	spc2egv	⊢ ( ( ∅ ∈ V ∧ { ⟨ 0 , 𝑁 ⟩ } ∈ V ) → ( ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 ) )
8	4 5 7	mpsyl	⊢ ( 𝑁 ∈ 𝑉 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 )