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

Metamath Proof Explorer

Theorem 0wlkons1

Description: A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021)

Ref Expression
Hypothesis 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0wlkons1 ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑁 ) ⟨“ 𝑁 ”⟩ )

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 s1val ⊢ ( 𝑁 ∈ 𝑉 → ⟨“ 𝑁 ”⟩ = { ⟨ 0 , 𝑁 ⟩ } )
3 0z ⊢ 0 ∈ ℤ
4 3 jctl ⊢ ( 𝑁 ∈ 𝑉 → ( 0 ∈ ℤ ∧ 𝑁 ∈ 𝑉 ) )
5 f1sng ⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ 𝑉 ) → { ⟨ 0 , 𝑁 ⟩ } : { 0 } –1-1→ 𝑉 )
6 f1f ⊢ ( { ⟨ 0 , 𝑁 ⟩ } : { 0 } –1-1→ 𝑉 → { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 )
7 4 5 6 3syl ⊢ ( 𝑁 ∈ 𝑉 → { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 )
8 id ⊢ ( ⟨“ 𝑁 ”⟩ = { ⟨ 0 , 𝑁 ⟩ } → ⟨“ 𝑁 ”⟩ = { ⟨ 0 , 𝑁 ⟩ } )
9 fzsn ⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
10 3 9 mp1i ⊢ ( ⟨“ 𝑁 ”⟩ = { ⟨ 0 , 𝑁 ⟩ } → ( 0 ... 0 ) = { 0 } )
11 8 10 feq12d ⊢ ( ⟨“ 𝑁 ”⟩ = { ⟨ 0 , 𝑁 ⟩ } → ( ⟨“ 𝑁 ”⟩ : ( 0 ... 0 ) ⟶ 𝑉 ↔ { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 ) )
12 7 11 syl5ibrcom ⊢ ( 𝑁 ∈ 𝑉 → ( ⟨“ 𝑁 ”⟩ = { ⟨ 0 , 𝑁 ⟩ } → ⟨“ 𝑁 ”⟩ : ( 0 ... 0 ) ⟶ 𝑉 ) )
13 2 12 mpd ⊢ ( 𝑁 ∈ 𝑉 → ⟨“ 𝑁 ”⟩ : ( 0 ... 0 ) ⟶ 𝑉 )
14 s1fv ⊢ ( 𝑁 ∈ 𝑉 → ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 )
15 1 0wlkon ⊢ ( ( ⟨“ 𝑁 ”⟩ : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑁 ) ⟨“ 𝑁 ”⟩ )
16 13 14 15 syl2anc ⊢ ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑁 ) ⟨“ 𝑁 ”⟩ )