Theorem upwordisword

Description: Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024)

	Ref	Expression
Assertion	upwordisword	|- ( A e. UpWord S -> A e. Word S )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( w = A -> ( w e. Word S <-> A e. Word S ) )
2		df-upword	|- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) }
3	2	abeq2i	|- ( w e. UpWord S <-> ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) )
4	3	simplbi	|- ( w e. UpWord S -> w e. Word S )
5	1 4	vtoclga	|- ( A e. UpWord S -> A e. Word S )