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	⊢ 𝑆 ∈ V
Assertion	upwordsseti	⊢ UpWord 𝑆 ∈ V

Proof

Step	Hyp	Ref	Expression
1		upwordsseti.1	⊢ 𝑆 ∈ V
2	1	wrdexi	⊢ Word 𝑆 ∈ V
3		upwordisword	⊢ ( 𝑡 ∈ UpWord 𝑆 → 𝑡 ∈ Word 𝑆 )
4	3	ssriv	⊢ UpWord 𝑆 ⊆ Word 𝑆
5	2 4	ssexi	⊢ UpWord 𝑆 ∈ V