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	⊢ ( 𝐴 ∈ Fin → { 𝑎 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		wrdnfi	⊢ ( 𝐴 ∈ Fin → { 𝑎 ∈ Word 𝐴 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )
2		id	⊢ ( 𝑎 ∈ ( < Chain 𝐴 ) → 𝑎 ∈ ( < Chain 𝐴 ) )
3	2	chnwrd	⊢ ( 𝑎 ∈ ( < Chain 𝐴 ) → 𝑎 ∈ Word 𝐴 )
4	3	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑎 ∈ ( < Chain 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑇 ) ) → 𝑎 ∈ Word 𝐴 )
5	4	rabss3d	⊢ ( ⊤ → { 𝑎 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ⊆ { 𝑎 ∈ Word 𝐴 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } )
6	5	mptru	⊢ { 𝑎 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ⊆ { 𝑎 ∈ Word 𝐴 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 }
7		ssfi	⊢ ( ( { 𝑎 ∈ Word 𝐴 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin ∧ { 𝑎 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ⊆ { 𝑎 ∈ Word 𝐴 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ) → { 𝑎 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )
8	1 6 7	sylancl	⊢ ( 𝐴 ∈ Fin → { 𝑎 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )