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 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 V F = P : 0 X P : 0 0 X
7 snssi X V X V
8 7 3ad2ant1 X V F = P : 0 X X V
9 6 8 fssd X V F = P : 0 X P : 0 0 V
10 breq1 F = F ClWalks G P ClWalks G P
11 10 3ad2ant2 X V F = P : 0 X F ClWalks G P ClWalks G P
12 1 1vgrex X V G V
13 1 0clwlk G V ClWalks G P P : 0 0 V
14 12 13 syl X V ClWalks G P P : 0 0 V
15 14 3ad2ant1 X V F = P : 0 X ClWalks G P P : 0 0 V
16 11 15 bitrd X V F = P : 0 X F ClWalks G P P : 0 0 V
17 9 16 mpbird X V F = P : 0 X F ClWalks G P