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 \mathrm{V}$$
Assertion	upwordsseti	Could not format assertion : No typesetting found for |- UpWord S e. _V with typecode |-

Proof

Step	Hyp	Ref	Expression
1		upwordsseti.1	$$⊢S\in \mathrm{V}$$
2	1	wrdexi	$$⊢\mathrm{Word}S\in \mathrm{V}$$
3		upwordisword	Could not format ( t e. UpWord S -> t e. Word S ) : No typesetting found for |- ( t e. UpWord S -> t e. Word S ) with typecode |-
4	3	ssriv	Could not format UpWord S C_ Word S : No typesetting found for |- UpWord S C_ Word S with typecode |-
5	2 4	ssexi	Could not format UpWord S e. _V : No typesetting found for |- UpWord S e. _V with typecode |-