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 ⊢ V = Vtx ⁡ G
Assertion 0wlkons1 ⊢ N ∈ V → ∅ N WalksOn ⁡ G N ⟨“ N ”⟩

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ V = Vtx ⁡ G
2 s1val ⊢ N ∈ V → ⟨“ N ”⟩ = 0 N
3 0z ⊢ 0 ∈ ℤ
4 3 jctl ⊢ N ∈ V → 0 ∈ ℤ ∧ N ∈ V
5 f1sng ⊢ 0 ∈ ℤ ∧ N ∈ V → 0 N : 0 ⟶ 1-1 V
6 f1f ⊢ 0 N : 0 ⟶ 1-1 V → 0 N : 0 ⟶ V
7 4 5 6 3syl ⊢ N ∈ V → 0 N : 0 ⟶ V
8 id ⊢ ⟨“ N ”⟩ = 0 N → ⟨“ N ”⟩ = 0 N
9 fzsn ⊢ 0 ∈ ℤ → 0 … 0 = 0
10 3 9 mp1i ⊢ ⟨“ N ”⟩ = 0 N → 0 … 0 = 0
11 8 10 feq12d ⊢ ⟨“ N ”⟩ = 0 N → ⟨“ N ”⟩ : 0 … 0 ⟶ V ↔ 0 N : 0 ⟶ V
12 7 11 syl5ibrcom ⊢ N ∈ V → ⟨“ N ”⟩ = 0 N → ⟨“ N ”⟩ : 0 … 0 ⟶ V
13 2 12 mpd ⊢ N ∈ V → ⟨“ N ”⟩ : 0 … 0 ⟶ V
14 s1fv ⊢ N ∈ V → ⟨“ N ”⟩ ⁡ 0 = N
15 1 0wlkon ⊢ ⟨“ N ”⟩ : 0 … 0 ⟶ V ∧ ⟨“ N ”⟩ ⁡ 0 = N → ∅ N WalksOn ⁡ G N ⟨“ N ”⟩
16 13 14 15 syl2anc ⊢ N ∈ V → ∅ N WalksOn ⁡ G N ⟨“ N ”⟩