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 \in Fin \to \{a \in UpWord S \| \|a\| = T\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		wrdnfi	$⊢ S \in Fin \to \{a \in Word S \| \|a\| = T\} \in Fin$
2		upwordisword	$⊢ a \in UpWord S \to a \in Word S$
3	2	ad2antrl	$⊢ (⊤ \land (a \in UpWord S \land \|a\| = T)) \to a \in Word S$
4	3	rabss3d	$⊢ ⊤ \to \{a \in UpWord S \| \|a\| = T\} \subseteq \{a \in Word S \| \|a\| = T\}$
5	4	mptru	$⊢ \{a \in UpWord S \| \|a\| = T\} \subseteq \{a \in Word S \| \|a\| = T\}$
6		ssfi	$⊢ (\{a \in Word S \| \|a\| = T\} \in Fin \land \{a \in UpWord S \| \|a\| = T\} \subseteq \{a \in Word S \| \|a\| = T\}) \to \{a \in UpWord S \| \|a\| = T\} \in Fin$
7	5 6	mpan2	$⊢ \{a \in Word S \| \|a\| = T\} \in Fin \to \{a \in UpWord S \| \|a\| = T\} \in Fin$
8	1 7	syl	$⊢ S \in Fin \to \{a \in UpWord S \| \|a\| = T\} \in Fin$