Definition df-upword 46472

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 46471	. 2 class UpWord𝑆
3		vw	. . . . . 6 setvar 𝑤
4	3	cv 1541	. . . . 5 class 𝑤
5	1	cword 14207	. . . . 5 class Word 𝑆
6	4, 5	wcel 2110	. . . 4 wff 𝑤 ∈ Word 𝑆
7		vk	. . . . . . . 8 setvar 𝑘
8	7	cv 1541	. . . . . . 7 class 𝑘
9	8, 4	cfv 6431	. . . . . 6 class (𝑤‘𝑘)
10		c1 10865	. . . . . . . 8 class 1
11		caddc 10867	. . . . . . . 8 class +
12	8, 10, 11	co 7269	. . . . . . 7 class (𝑘 + 1)
13	12, 4	cfv 6431	. . . . . 6 class (𝑤‘(𝑘 + 1))
14		clt 11002	. . . . . 6 class <
15	9, 13, 14	wbr 5079	. . . . 5 wff (𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
16		cc0 10864	. . . . . 6 class 0
17		chash 14034	. . . . . . . 8 class ♯
18	4, 17	cfv 6431	. . . . . . 7 class (♯‘𝑤)
19		cmin 11197	. . . . . . 7 class −
20	18, 10, 19	co 7269	. . . . . 6 class ((♯‘𝑤) − 1)
21		cfzo 13373	. . . . . 6 class ..^
22	16, 20, 21	co 7269	. . . . 5 class (0..^((♯‘𝑤) − 1))
23	15, 7, 22	wral 3066	. . . 4 wff ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1))
24	6, 23	wa 396	. . 3 wff (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))
25	24, 3	cab 2717	. 2 class {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}
26	2, 25	wceq 1542	1 wff UpWord𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}

This definition is referenced by:  upwordnul  46473  upwordisword  46474