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 e. Fin -> { a e. ( .< Chain A ) | ( # ` a ) = T } e. Fin )

Proof

Step	Hyp	Ref	Expression
1		wrdnfi	|- ( A e. Fin -> { a e. Word A | ( # ` a ) = T } e. Fin )
2		id	|- ( a e. ( .< Chain A ) -> a e. ( .< Chain A ) )
3	2	chnwrd	|- ( a e. ( .< Chain A ) -> a e. Word A )
4	3	ad2antrl	|- ( ( T. /\ ( a e. ( .< Chain A ) /\ ( # ` a ) = T ) ) -> a e. Word A )
5	4	rabss3d	|- ( T. -> { a e. ( .< Chain A ) | ( # ` a ) = T } C_ { a e. Word A | ( # ` a ) = T } )
6	5	mptru	|- { a e. ( .< Chain A ) | ( # ` a ) = T } C_ { a e. Word A | ( # ` a ) = T }
7		ssfi	|- ( ( { a e. Word A | ( # ` a ) = T } e. Fin /\ { a e. ( .< Chain A ) | ( # ` a ) = T } C_ { a e. Word A | ( # ` a ) = T } ) -> { a e. ( .< Chain A ) | ( # ` a ) = T } e. Fin )
8	1 6 7	sylancl	|- ( A e. Fin -> { a e. ( .< Chain A ) | ( # ` a ) = T } e. Fin )