Theorem chnflenfi

Description: There is a finite number of chains with fixed length over finite alphabet. Trivially holds for invalid lengths as there're no matching sequences. (Contributed by Ender Ting, 5-Jan-2025) (Revised by Ender Ting, 17-Jan-2026)

	Ref	Expression
Assertion	chnflenfi	$$⊢A\in \mathrm{Fin}\to \left\{a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}|\left|a\right|=T\right\}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		wrdnfi	$$⊢A\in \mathrm{Fin}\to \left\{a\in \mathrm{Word}A|\left|a\right|=T\right\}\in \mathrm{Fin}$$
2		id	$$⊢a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
3	2	chnwrd	$$⊢a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to a\in \mathrm{Word}A$$
4	3	ad2antrl	$$⊢\left(\top \wedge \left(a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\wedge \left|a\right|=T\right)\right)\to a\in \mathrm{Word}A$$
5	4	rabss3d	$$⊢\top \to \left\{a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}|\left|a\right|=T\right\}\subseteq \left\{a\in \mathrm{Word}A|\left|a\right|=T\right\}$$
6	5	mptru	$$⊢\left\{a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}|\left|a\right|=T\right\}\subseteq \left\{a\in \mathrm{Word}A|\left|a\right|=T\right\}$$
7		ssfi	$$⊢\left(\left\{a\in \mathrm{Word}A|\left|a\right|=T\right\}\in \mathrm{Fin}\wedge \left\{a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}|\left|a\right|=T\right\}\subseteq \left\{a\in \mathrm{Word}A|\left|a\right|=T\right\}\right)\to \left\{a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}|\left|a\right|=T\right\}\in \mathrm{Fin}$$
8	1 6 7	sylancl	$$⊢A\in \mathrm{Fin}\to \left\{a\in {\mathrm{Chain}}_A\underset{\dot{}}{<}|\left|a\right|=T\right\}\in \mathrm{Fin}$$