Theorem 0clwlk

Description: A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 17-Feb-2021) (Revised by AV, 30-Oct-2021)

	Ref	Expression
Hypothesis	0clwlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	0clwlk	$$⊢G\in X\to \left(\varnothing \mathrm{ClWalks}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$

Proof

Step	Hyp	Ref	Expression
1		0clwlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	0wlk	$$⊢G\in X\to \left(\varnothing \mathrm{Walks}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$
3	2	anbi2d	$$⊢G\in X\to \left(\left(P\left(0\right)=P\left(\left|\varnothing \right|\right)\wedge \varnothing \mathrm{Walks}\left(G\right)P\right)\leftrightarrow \left(P\left(0\right)=P\left(\left|\varnothing \right|\right)\wedge P:\left(0\dots 0\right)⟶V\right)\right)$$
4		isclwlk	$$⊢\varnothing \mathrm{ClWalks}\left(G\right)P\leftrightarrow \left(\varnothing \mathrm{Walks}\left(G\right)P\wedge P\left(0\right)=P\left(\left|\varnothing \right|\right)\right)$$
5	4	biancomi	$$⊢\varnothing \mathrm{ClWalks}\left(G\right)P\leftrightarrow \left(P\left(0\right)=P\left(\left|\varnothing \right|\right)\wedge \varnothing \mathrm{Walks}\left(G\right)P\right)$$
6		hash0	$$⊢\left|\varnothing \right|=0$$
7	6	eqcomi	$$⊢0=\left|\varnothing \right|$$
8	7	fveq2i	$$⊢P\left(0\right)=P\left(\left|\varnothing \right|\right)$$
9	8	biantrur	$$⊢P:\left(0\dots 0\right)⟶V\leftrightarrow \left(P\left(0\right)=P\left(\left|\varnothing \right|\right)\wedge P:\left(0\dots 0\right)⟶V\right)$$
10	3 5 9	3bitr4g	$$⊢G\in X\to \left(\varnothing \mathrm{ClWalks}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$