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 )