Definition df-upword 46758

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 46757	. 2 class UpWord𝑆
3		vw	. . . . . 6 setvar 𝑤
4	3	cv 1538	. . . . 5 class 𝑤
5	1	cword 14266	. . . . 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 6458	. . . . . 6 class (𝑤‘𝑘)
10		c1 10922	. . . . . . . 8 class 1
11		caddc 10924	. . . . . . . 8 class +
12	8, 10, 11	co 7307	. . . . . . 7 class (𝑘 + 1)
13	12, 4	cfv 6458	. . . . . 6 class (𝑤‘(𝑘 + 1))
14		clt 11059	. . . . . 6 class <
15	9, 13, 14	wbr 5081	. . . . 5 wff (𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
16		cc0 10921	. . . . . 6 class 0
17		chash 14094	. . . . . . . 8 class ♯
18	4, 17	cfv 6458	. . . . . . 7 class (♯‘𝑤)
19		cmin 11255	. . . . . . 7 class −
20	18, 10, 19	co 7307	. . . . . 6 class ((♯‘𝑤) − 1)
21		cfzo 13432	. . . . . 6 class ..^
22	16, 20, 21	co 7307	. . . . 5 class (0..^((♯‘𝑤) − 1))
23	15, 7, 22	wral 3062	. . . 4 wff ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
24	6, 23	wa 397	. . 3 wff (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))
25	24, 3	cab 2713	. 2 class {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}
26	2, 25	wceq 1539	1 wff UpWord𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}

This definition is referenced by:  upwordnul  46759  upwordisword  46760  upwordsing  46763  tworepnotupword  46765