Definition df-upword 45583

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 45582	. 2 class UpWord 𝑆
3		vw	. . . . . 6 setvar 𝑤
4	3	cv 1540	. . . . 5 class 𝑤
5	1	cword 14463	. . . . 5 class Word 𝑆
6	4, 5	wcel 2106	. . . 4 wff 𝑤 ∈ Word 𝑆
7		vk	. . . . . . . 8 setvar 𝑘
8	7	cv 1540	. . . . . . 7 class 𝑘
9	8, 4	cfv 6543	. . . . . 6 class (𝑤‘𝑘)
10		c1 11110	. . . . . . . 8 class 1
11		caddc 11112	. . . . . . . 8 class +
12	8, 10, 11	co 7408	. . . . . . 7 class (𝑘 + 1)
13	12, 4	cfv 6543	. . . . . 6 class (𝑤‘(𝑘 + 1))
14		clt 11247	. . . . . 6 class <
15	9, 13, 14	wbr 5148	. . . . 5 wff (𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
16		cc0 11109	. . . . . 6 class 0
17		chash 14289	. . . . . . . 8 class ♯
18	4, 17	cfv 6543	. . . . . . 7 class (♯‘𝑤)
19		cmin 11443	. . . . . . 7 class −
20	18, 10, 19	co 7408	. . . . . 6 class ((♯‘𝑤) − 1)
21		cfzo 13626	. . . . . 6 class ..^
22	16, 20, 21	co 7408	. . . . 5 class (0..^((♯‘𝑤) − 1))
23	15, 7, 22	wral 3061	. . . 4 wff ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
24	6, 23	wa 396	. . 3 wff (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))
25	24, 3	cab 2709	. 2 class {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}
26	2, 25	wceq 1541	1 wff UpWord 𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}

This definition is referenced by:  upwordnul  45584  upwordisword  45585  upwordsing  45588  tworepnotupword  45590