Definition df-upword 45891

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 45890	. 2 class UpWord 𝑆
3		vw	. . . . . 6 setvar 𝑤
4	3	cv 1538	. . . . 5 class 𝑤
5	1	cword 14468	. . . . 5 class Word 𝑆
6	4, 5	wcel 2104	. . . 4 wff 𝑤 ∈ Word 𝑆
7		vk	. . . . . . . 8 setvar 𝑘
8	7	cv 1538	. . . . . . 7 class 𝑘
9	8, 4	cfv 6542	. . . . . 6 class (𝑤‘𝑘)
10		c1 11113	. . . . . . . 8 class 1
11		caddc 11115	. . . . . . . 8 class +
12	8, 10, 11	co 7411	. . . . . . 7 class (𝑘 + 1)
13	12, 4	cfv 6542	. . . . . 6 class (𝑤‘(𝑘 + 1))
14		clt 11252	. . . . . 6 class <
15	9, 13, 14	wbr 5147	. . . . 5 wff (𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
16		cc0 11112	. . . . . 6 class 0
17		chash 14294	. . . . . . . 8 class ♯
18	4, 17	cfv 6542	. . . . . . 7 class (♯‘𝑤)
19		cmin 11448	. . . . . . 7 class −
20	18, 10, 19	co 7411	. . . . . 6 class ((♯‘𝑤) − 1)
21		cfzo 13631	. . . . . 6 class ..^
22	16, 20, 21	co 7411	. . . . 5 class (0..^((♯‘𝑤) − 1))
23	15, 7, 22	wral 3059	. . . 4 wff ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
24	6, 23	wa 394	. . 3 wff (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))
25	24, 3	cab 2707	. 2 class {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}
26	2, 25	wceq 1539	1 wff UpWord 𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}

This definition is referenced by:  upwordnul  45892  upwordisword  45893  upwordsing  45896  tworepnotupword  45898