Theorem upwrdfi

Description: There is a finite number of strictly increasing sequences of a given length over finite alphabet. Trivially holds for invalid lengths where there're zero matching sequences. (Contributed by Ender Ting, 5-Jan-2024)

	Ref	Expression
Assertion	upwrdfi	⊢ ( 𝑆 ∈ Fin → { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		wrdnfi	⊢ ( 𝑆 ∈ Fin → { 𝑎 ∈ Word 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )
2		upwordisword	⊢ ( 𝑎 ∈ UpWord 𝑆 → 𝑎 ∈ Word 𝑆 )
3	2	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑎 ∈ UpWord 𝑆 ∧ ( ♯ ‘ 𝑎 ) = 𝑇 ) ) → 𝑎 ∈ Word 𝑆 )
4	3	rabss3d	⊢ ( ⊤ → { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ⊆ { 𝑎 ∈ Word 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } )
5	4	mptru	⊢ { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ⊆ { 𝑎 ∈ Word 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 }
6		ssfi	⊢ ( ( { 𝑎 ∈ Word 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin ∧ { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ⊆ { 𝑎 ∈ Word 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ) → { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )
7	5 6	mpan2	⊢ ( { 𝑎 ∈ Word 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin → { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )
8	1 7	syl	⊢ ( 𝑆 ∈ Fin → { 𝑎 ∈ UpWord 𝑆 ∣ ( ♯ ‘ 𝑎 ) = 𝑇 } ∈ Fin )