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

Metamath Proof Explorer

Theorem 0clwlkv

Description: Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022)

Ref Expression
Hypothesis 0clwlk.v 
|- V = ( Vtx ` G )
Assertion 0clwlkv 
|- ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> F ( ClWalks ` G ) P )

Proof

Step Hyp Ref Expression
1 0clwlk.v 
 |-  V = ( Vtx ` G )
2 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
3 2 eqcomi 
 |-  { 0 } = ( 0 ... 0 )
4 3 feq2i 
 |-  ( P : { 0 } --> { X } <-> P : ( 0 ... 0 ) --> { X } )
5 4 biimpi 
 |-  ( P : { 0 } --> { X } -> P : ( 0 ... 0 ) --> { X } )
6 5 3ad2ant3 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> P : ( 0 ... 0 ) --> { X } )
7 snssi 
 |-  ( X e. V -> { X } C_ V )
8 7 3ad2ant1 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> { X } C_ V )
9 6 8 fssd 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> P : ( 0 ... 0 ) --> V )
10 breq1 
 |-  ( F = (/) -> ( F ( ClWalks ` G ) P <-> (/) ( ClWalks ` G ) P ) )
11 10 3ad2ant2 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> ( F ( ClWalks ` G ) P <-> (/) ( ClWalks ` G ) P ) )
12 1 1vgrex 
 |-  ( X e. V -> G e. _V )
13 1 0clwlk 
 |-  ( G e. _V -> ( (/) ( ClWalks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
14 12 13 syl 
 |-  ( X e. V -> ( (/) ( ClWalks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
15 14 3ad2ant1 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> ( (/) ( ClWalks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
16 11 15 bitrd 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> ( F ( ClWalks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
17 9 16 mpbird 
 |-  ( ( X e. V /\ F = (/) /\ P : { 0 } --> { X } ) -> F ( ClWalks ` G ) P )