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 "> )