Definition df-upword 46851

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

Assertion

Ref	Expression
df-upword	⊢ UpWord 𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}

Distinct variable group:   𝑆,𝑘,𝑤

Detailed syntax breakdown of Definition df-upword

Step	Hyp	Ref	Expression
1		cS	. . 3 class 𝑆
2	1	cupword 46850	. 2 class UpWord 𝑆
3		vw	. . . . . 6 setvar 𝑤
4	3	cv 1538	. . . . 5 class 𝑤
5	1	cword 14534	. . . . 5 class Word 𝑆
6	4, 5	wcel 2107	. . . 4 wff 𝑤 ∈ Word 𝑆
7		vk	. . . . . . . 8 setvar 𝑘
8	7	cv 1538	. . . . . . 7 class 𝑘
9	8, 4	cfv 6541	. . . . . 6 class (𝑤‘𝑘)
10		c1 11138	. . . . . . . 8 class 1
11		caddc 11140	. . . . . . . 8 class +
12	8, 10, 11	co 7413	. . . . . . 7 class (𝑘 + 1)
13	12, 4	cfv 6541	. . . . . 6 class (𝑤‘(𝑘 + 1))
14		clt 11277	. . . . . 6 class <
15	9, 13, 14	wbr 5123	. . . . 5 wff (𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
16		cc0 11137	. . . . . 6 class 0
17		chash 14351	. . . . . . . 8 class ♯
18	4, 17	cfv 6541	. . . . . . 7 class (♯‘𝑤)
19		cmin 11474	. . . . . . 7 class −
20	18, 10, 19	co 7413	. . . . . 6 class ((♯‘𝑤) − 1)
21		cfzo 13676	. . . . . 6 class ..^
22	16, 20, 21	co 7413	. . . . 5 class (0..^((♯‘𝑤) − 1))
23	15, 7, 22	wral 3050	. . . 4 wff ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
24	6, 23	wa 395	. . 3 wff (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))
25	24, 3	cab 2712	. 2 class {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}
26	2, 25	wceq 1539	1 wff UpWord 𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}

This definition is referenced by:  upwordnul  46852  upwordisword  46853  upwordsing  46856  tworepnotupword  46858