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 ‘ 𝐺 ) 𝑁 ) 𝑝 )