Metamath Proof Explorer

Theorem upwordsseti

Description: Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024)

		Ref	Expression
	Hypothesis	upwordsseti.1	$⊢ S \in V$
	Assertion	upwordsseti	$⊢ UpWord S \in V$

Step	Hyp	Ref	Expression
1		upwordsseti.1	$⊢ S \in V$
2	1	wrdexi	$⊢ Word S \in V$
3		upwordisword	$⊢ t \in UpWord S \to t \in Word S$
4	3	ssriv	$⊢ UpWord S \subseteq Word S$
5	2 4	ssexi	$⊢ UpWord S \in V$