Metamath Proof Explorer

Definition df-upword

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

Ref Expression
Assertion df-upword ⊢ UpWord S = w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cS class S
1 0 cupword class UpWord S
2 vw setvar w
3 2 cv setvar w
4 0 cword class Word S
5 3 4 wcel wff w ∈ Word S
6 vk setvar k
7 cc0 class 0
8 cfzo class ..^
9 chash class .
10 3 9 cfv class w
11 cmin class −
12 c1 class 1
13 10 12 11 co class w − 1
14 7 13 8 co class 0 ..^ w − 1
15 6 cv setvar k
16 15 3 cfv class w ⁡ k
17 clt class <
18 caddc class +
19 15 12 18 co class k + 1
20 19 3 cfv class w ⁡ k + 1
21 16 20 17 wbr wff w ⁡ k < w ⁡ k + 1
22 21 6 14 wral wff ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
23 5 22 wa wff w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
24 23 2 cab class w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
25 1 24 wceq wff UpWord S = w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1