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	⊢ UpWord 𝑆 = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cS	⊢ 𝑆
1	0	cupword	⊢ UpWord 𝑆
2		vw	⊢ 𝑤
3	2	cv	⊢ 𝑤
4	0	cword	⊢ Word 𝑆
5	3 4	wcel	⊢ 𝑤 ∈ Word 𝑆
6		vk	⊢ 𝑘
7		cc0	⊢ 0
8		cfzo	⊢ ..^
9		chash	⊢ ♯
10	3 9	cfv	⊢ ( ♯ ‘ 𝑤 )
11		cmin	⊢ −
12		c1	⊢ 1
13	10 12 11	co	⊢ ( ( ♯ ‘ 𝑤 ) − 1 )
14	7 13 8	co	⊢ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) )
15	6	cv	⊢ 𝑘
16	15 3	cfv	⊢ ( 𝑤 ‘ 𝑘 )
17		clt	⊢ <
18		caddc	⊢ +
19	15 12 18	co	⊢ ( 𝑘 + 1 )
20	19 3	cfv	⊢ ( 𝑤 ‘ ( 𝑘 + 1 ) )
21	16 20 17	wbr	⊢ ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) )
22	21 6 14	wral	⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) )
23	5 22	wa	⊢ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) )
24	23 2	cab	⊢ { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) }
25	1 24	wceq	⊢ UpWord 𝑆 = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) }