Theorem clwlkwlk

Description: Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 16-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	clwlkwlk	$$⊢W\in \mathrm{ClWalks}\left(G\right)\to W\in \mathrm{Walks}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		elopabran	$$⊢W\in \left\{⟨f,p⟩|\left(f\mathrm{Walks}\left(G\right)p\wedge p\left(0\right)=p\left(\left|f\right|\right)\right)\right\}\to W\in \mathrm{Walks}\left(G\right)$$
2		clwlks	$$⊢\mathrm{ClWalks}\left(G\right)=\left\{⟨f,p⟩|\left(f\mathrm{Walks}\left(G\right)p\wedge p\left(0\right)=p\left(\left|f\right|\right)\right)\right\}$$
3	1 2	eleq2s	$$⊢W\in \mathrm{ClWalks}\left(G\right)\to W\in \mathrm{Walks}\left(G\right)$$