Definition df-upword

Description: Strictly increasing sequence is a sequence, adjacent elements of which increase. (Contributed by Ender Ting, 19-Nov-2024)

	Ref	Expression
Assertion	df-upword	Could not format assertion : No typesetting found for |- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cS	$$classS$$
1	0	cupword	Could not format UpWord S : No typesetting found for class UpWord S with typecode class
2		vw	$$setvarw$$
3	2	cv	$$setvarw$$
4	0	cword	$$class\mathrm{Word}S$$
5	3 4	wcel	$$wffw\in \mathrm{Word}S$$
6		vk	$$setvark$$
7		cc0	$$class0$$
8		cfzo	$$class..^$$
9		chash	$$class\left|.\right|$$
10	3 9	cfv	$$class\left|w\right|$$
11		cmin	$$class-$$
12		c1	$$class1$$
13	10 12 11	co	$$class\left(\left|w\right|-1\right)$$
14	7 13 8	co	$$class\left(0..^\left|w\right|-1\right)$$
15	6	cv	$$setvark$$
16	15 3	cfv	$$classw\left(k\right)$$
17		clt	$$class<$$
18		caddc	$$class+$$
19	15 12 18	co	$$class\left(k+1\right)$$
20	19 3	cfv	$$classw\left(k+1\right)$$
21	16 20 17	wbr	$$wffw\left(k\right)<w\left(k+1\right)$$
22	21 6 14	wral	$$wff\forall k\in \left(0..^\left|w\right|-1\right)w\left(k\right)<w\left(k+1\right)$$
23	5 22	wa	$$wff\left(w\in \mathrm{Word}S\wedge \forall k\in \left(0..^\left|w\right|-1\right)w\left(k\right)<w\left(k+1\right)\right)$$
24	23 2	cab	$$class\left\{w|\left(w\in \mathrm{Word}S\wedge \forall k\in \left(0..^\left|w\right|-1\right)w\left(k\right)<w\left(k+1\right)\right)\right\}$$
25	1 24	wceq	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 wff UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } with typecode wff