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 e. V -> (/) ( N ( WalksOn ` G ) N ) <" N "> )

Proof

Step Hyp Ref Expression
1 0wlk.v 
 |-  V = ( Vtx ` G )
2 s1val 
 |-  ( N e. V -> <" N "> = { <. 0 , N >. } )
3 0z 
 |-  0 e. ZZ
4 3 jctl 
 |-  ( N e. V -> ( 0 e. ZZ /\ N e. V ) )
5 f1sng 
 |-  ( ( 0 e. ZZ /\ N e. 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 e. V -> { <. 0 , N >. } : { 0 } --> V )
8 id 
 |-  ( <" N "> = { <. 0 , N >. } -> <" N "> = { <. 0 , N >. } )
9 fzsn 
 |-  ( 0 e. ZZ -> ( 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 e. V -> ( <" N "> = { <. 0 , N >. } -> <" N "> : ( 0 ... 0 ) --> V ) )
13 2 12 mpd 
 |-  ( N e. V -> <" N "> : ( 0 ... 0 ) --> V )
14 s1fv 
 |-  ( N e. 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 e. V -> (/) ( N ( WalksOn ` G ) N ) <" N "> )