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

Proof

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