Theorem clwlknf1oclwwlknlem2

Description: Lemma 2 for clwlknf1oclwwlkn : The closed walks of a positive length are nonempty closed walks of this length. (Contributed by AV, 26-May-2022)

	Ref	Expression
Assertion	clwlknf1oclwwlknlem2	$$⊢N\in \mathbb{N}\to \left\{w\in \mathrm{ClWalks}\left(G\right)|\left|1^{st}\left(w\right)\right|=N\right\}=\left\{c\in \mathrm{ClWalks}\left(G\right)|\left(1\le \left|1^{st}\left(c\right)\right|\wedge \left|1^{st}\left(c\right)\right|=N\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		2fveq3	$$⊢w=c\to \left|1^{st}\left(w\right)\right|=\left|1^{st}\left(c\right)\right|$$
2	1	eqeq1d	$$⊢w=c\to \left(\left|1^{st}\left(w\right)\right|=N\leftrightarrow \left|1^{st}\left(c\right)\right|=N\right)$$
3	2	cbvrabv	$$⊢\left\{w\in \mathrm{ClWalks}\left(G\right)|\left|1^{st}\left(w\right)\right|=N\right\}=\left\{c\in \mathrm{ClWalks}\left(G\right)|\left|1^{st}\left(c\right)\right|=N\right\}$$
4		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
5		breq2	$$⊢\left|1^{st}\left(c\right)\right|=N\to \left(1\le \left|1^{st}\left(c\right)\right|\leftrightarrow 1\le N\right)$$
6	4 5	syl5ibrcom	$$⊢N\in \mathbb{N}\to \left(\left|1^{st}\left(c\right)\right|=N\to 1\le \left|1^{st}\left(c\right)\right|\right)$$
7	6	pm4.71rd	$$⊢N\in \mathbb{N}\to \left(\left|1^{st}\left(c\right)\right|=N\leftrightarrow \left(1\le \left|1^{st}\left(c\right)\right|\wedge \left|1^{st}\left(c\right)\right|=N\right)\right)$$
8	7	rabbidv	$$⊢N\in \mathbb{N}\to \left\{c\in \mathrm{ClWalks}\left(G\right)|\left|1^{st}\left(c\right)\right|=N\right\}=\left\{c\in \mathrm{ClWalks}\left(G\right)|\left(1\le \left|1^{st}\left(c\right)\right|\wedge \left|1^{st}\left(c\right)\right|=N\right)\right\}$$
9	3 8	syl5eq	$$⊢N\in \mathbb{N}\to \left\{w\in \mathrm{ClWalks}\left(G\right)|\left|1^{st}\left(w\right)\right|=N\right\}=\left\{c\in \mathrm{ClWalks}\left(G\right)|\left(1\le \left|1^{st}\left(c\right)\right|\wedge \left|1^{st}\left(c\right)\right|=N\right)\right\}$$