Theorem upwordisword

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

	Ref	Expression
Assertion	upwordisword	Could not format assertion : No typesetting found for |- ( A e. UpWord S -> A e. Word S ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢w=A\to \left(w\in \mathrm{Word}S\leftrightarrow A\in \mathrm{Word}S\right)$$
2		df-upword	Could not format UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } : No typesetting found for |- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } with typecode |-
3	2	abeq2i	Could not format ( w e. UpWord S <-> ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) ) : No typesetting found for |- ( w e. UpWord S <-> ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) ) with typecode |-
4	3	simplbi	Could not format ( w e. UpWord S -> w e. Word S ) : No typesetting found for |- ( w e. UpWord S -> w e. Word S ) with typecode |-
5	1 4	vtoclga	Could not format ( A e. UpWord S -> A e. Word S ) : No typesetting found for |- ( A e. UpWord S -> A e. Word S ) with typecode |-