Theorem clwwlknfi

Description: If there is only a finite number of vertices, the number of closed walks of fixed length (as words) is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022) (Proof shortened by JJ, 18-Nov-2022)

	Ref	Expression
Assertion	clwwlknfi	$$⊢\mathrm{Vtx}\left(G\right)\in \mathrm{Fin}\to N\mathrm{ClWWalksN}G\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		clwwlkn	$$⊢N\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$
2		wrdnfi	$$⊢\mathrm{Vtx}\left(G\right)\in \mathrm{Fin}\to \left\{w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)|\left|w\right|=N\right\}\in \mathrm{Fin}$$
3		clwwlksswrd	$$⊢\mathrm{ClWWalks}\left(G\right)\subseteq \mathrm{Word}\mathrm{Vtx}\left(G\right)$$
4		rabss2	$$⊢\mathrm{ClWWalks}\left(G\right)\subseteq \mathrm{Word}\mathrm{Vtx}\left(G\right)\to \left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}\subseteq \left\{w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)|\left|w\right|=N\right\}$$
5	3 4	mp1i	$$⊢\mathrm{Vtx}\left(G\right)\in \mathrm{Fin}\to \left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}\subseteq \left\{w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)|\left|w\right|=N\right\}$$
6	2 5	ssfid	$$⊢\mathrm{Vtx}\left(G\right)\in \mathrm{Fin}\to \left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}\in \mathrm{Fin}$$
7	1 6	eqeltrid	$$⊢\mathrm{Vtx}\left(G\right)\in \mathrm{Fin}\to N\mathrm{ClWWalksN}G\in \mathrm{Fin}$$