Metamath Proof Explorer

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	5 6	mpan2	\|- ( { a e. Word S \| ( # ` a ) = T } e. Fin -> { a e. UpWord S \| ( # ` a ) = T } e. Fin )
8	1 7	syl	\|- ( S e. Fin -> { a e. UpWord S \| ( # ` a ) = T } e. Fin )