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 ‘ 𝐺 ) 𝑁 ) ⟨“ 𝑁 ”⟩ )