Theorem iswwlksn

Description: A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

	Ref	Expression
Assertion	iswwlksn	$$⊢N\in {\mathbb{N}}_0\to \left(W\in \left(N\mathrm{WWalksN}G\right)\leftrightarrow \left(W\in \mathrm{WWalks}\left(G\right)\wedge \left|W\right|=N+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		wwlksn	$$⊢N\in {\mathbb{N}}_0\to N\mathrm{WWalksN}G=\left\{w\in \mathrm{WWalks}\left(G\right)|\left|w\right|=N+1\right\}$$
2	1	eleq2d	$$⊢N\in {\mathbb{N}}_0\to \left(W\in \left(N\mathrm{WWalksN}G\right)\leftrightarrow W\in \left\{w\in \mathrm{WWalks}\left(G\right)|\left|w\right|=N+1\right\}\right)$$
3		fveqeq2	$$⊢w=W\to \left(\left|w\right|=N+1\leftrightarrow \left|W\right|=N+1\right)$$
4	3	elrab	$$⊢W\in \left\{w\in \mathrm{WWalks}\left(G\right)|\left|w\right|=N+1\right\}\leftrightarrow \left(W\in \mathrm{WWalks}\left(G\right)\wedge \left|W\right|=N+1\right)$$
5	2 4	bitrdi	$$⊢N\in {\mathbb{N}}_0\to \left(W\in \left(N\mathrm{WWalksN}G\right)\leftrightarrow \left(W\in \mathrm{WWalks}\left(G\right)\wedge \left|W\right|=N+1\right)\right)$$