Theorem wlknwwlksneqs

Description: The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 15-Apr-2021)

	Ref	Expression
Assertion	wlknwwlksneqs	$$⊢\left(G\in \mathrm{USHGraph}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{p\in \mathrm{Walks}\left(G\right)|\left|1^{st}\left(p\right)\right|=N\right\}\right|=\left|N\mathrm{WWalksN}G\right|$$

Proof

Step	Hyp	Ref	Expression
1		wlknwwlksnen	$$⊢\left(G\in \mathrm{USHGraph}\wedge N\in {\mathbb{N}}_0\right)\to \left\{p\in \mathrm{Walks}\left(G\right)|\left|1^{st}\left(p\right)\right|=N\right\}\approx \left(N\mathrm{WWalksN}G\right)$$
2		hasheni	$$⊢\left\{p\in \mathrm{Walks}\left(G\right)|\left|1^{st}\left(p\right)\right|=N\right\}\approx \left(N\mathrm{WWalksN}G\right)\to \left|\left\{p\in \mathrm{Walks}\left(G\right)|\left|1^{st}\left(p\right)\right|=N\right\}\right|=\left|N\mathrm{WWalksN}G\right|$$
3	1 2	syl	$$⊢\left(G\in \mathrm{USHGraph}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{p\in \mathrm{Walks}\left(G\right)|\left|1^{st}\left(p\right)\right|=N\right\}\right|=\left|N\mathrm{WWalksN}G\right|$$