Theorem wrdnfi

Description: If there is only a finite number of symbols, the number of words of a fixed length over these symbols is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018) Remove unnecessary antecedent. (Revised by JJ, 18-Nov-2022)

	Ref	Expression
Assertion	wrdnfi	$$⊢V\in \mathrm{Fin}\to \left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		hashwrdn	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|={\left|V\right|}^N$$
2		hashcl	$$⊢V\in \mathrm{Fin}\to \left|V\right|\in {\mathbb{N}}_0$$
3		nn0expcl	$$⊢\left(\left|V\right|\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to {\left|V\right|}^N\in {\mathbb{N}}_0$$
4	2 3	sylan	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to {\left|V\right|}^N\in {\mathbb{N}}_0$$
5	1 4	eqeltrd	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|\in {\mathbb{N}}_0$$
6	5	ex	$$⊢V\in \mathrm{Fin}\to \left(N\in {\mathbb{N}}_0\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|\in {\mathbb{N}}_0\right)$$
7		lencl	$$⊢w\in \mathrm{Word}V\to \left|w\right|\in {\mathbb{N}}_0$$
8		eleq1	$$⊢\left|w\right|=N\to \left(\left|w\right|\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{N}}_0\right)$$
9	7 8	syl5ibcom	$$⊢w\in \mathrm{Word}V\to \left(\left|w\right|=N\to N\in {\mathbb{N}}_0\right)$$
10	9	con3rr3	$$⊢\neg N\in {\mathbb{N}}_0\to \left(w\in \mathrm{Word}V\to \neg \left|w\right|=N\right)$$
11	10	ralrimiv	$$⊢\neg N\in {\mathbb{N}}_0\to \forall w\in \mathrm{Word}V\neg \left|w\right|=N$$
12		rabeq0	$$⊢\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}=\varnothing \leftrightarrow \forall w\in \mathrm{Word}V\neg \left|w\right|=N$$
13	11 12	sylibr	$$⊢\neg N\in {\mathbb{N}}_0\to \left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}=\varnothing$$
14	13	fveq2d	$$⊢\neg N\in {\mathbb{N}}_0\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|=\left|\varnothing \right|$$
15		hash0	$$⊢\left|\varnothing \right|=0$$
16	14 15	eqtrdi	$$⊢\neg N\in {\mathbb{N}}_0\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|=0$$
17		0nn0	$$⊢0\in {\mathbb{N}}_0$$
18	16 17	eqeltrdi	$$⊢\neg N\in {\mathbb{N}}_0\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|\in {\mathbb{N}}_0$$
19	6 18	pm2.61d1	$$⊢V\in \mathrm{Fin}\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|\in {\mathbb{N}}_0$$
20		wrdexg	$$⊢V\in \mathrm{Fin}\to \mathrm{Word}V\in \mathrm{V}$$
21		rabexg	$$⊢\mathrm{Word}V\in \mathrm{V}\to \left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\in \mathrm{V}$$
22		hashclb	$$⊢\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\in \mathrm{V}\to \left(\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\in \mathrm{Fin}\leftrightarrow \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|\in {\mathbb{N}}_0\right)$$
23	20 21 22	3syl	$$⊢V\in \mathrm{Fin}\to \left(\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\in \mathrm{Fin}\leftrightarrow \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|\in {\mathbb{N}}_0\right)$$
24	19 23	mpbird	$$⊢V\in \mathrm{Fin}\to \left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\in \mathrm{Fin}$$