This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0pthon1 ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )

Proof

Step Hyp Ref Expression
1 0pthon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqidd ⊢ ( 𝑁 ∈ 𝑉 → { ⟨ 0 , 𝑁 ⟩ } = { ⟨ 0 , 𝑁 ⟩ } )
3 1fv ⊢ ( ( 𝑁 ∈ 𝑉 ∧ { ⟨ 0 , 𝑁 ⟩ } = { ⟨ 0 , 𝑁 ⟩ } ) → ( { ⟨ 0 , 𝑁 ⟩ } : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
4 2 3 mpdan ⊢ ( 𝑁 ∈ 𝑉 → ( { ⟨ 0 , 𝑁 ⟩ } : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
5 1 0pthon ⊢ ( ( { ⟨ 0 , 𝑁 ⟩ } : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )
6 4 5 syl ⊢ ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )