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 e. _V
Assertion upwordsseti 
|- UpWord S e. _V

Proof

Step Hyp Ref Expression
1 upwordsseti.1 
 |-  S e. _V
2 1 wrdexi 
 |-  Word S e. _V
3 upwordisword 
 |-  ( t e. UpWord S -> t e. Word S )
4 3 ssriv 
 |-  UpWord S C_ Word S
5 2 4 ssexi 
 |-  UpWord S e. _V