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 e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cS 
 |-  S
1 0 cupword 
 |-  UpWord S
2 vw 
 |-  w
3 2 cv 
 |-  w
4 0 cword 
 |-  Word S
5 3 4 wcel 
 |-  w e. Word S
6 vk 
 |-  k
7 cc0 
 |-  0
8 cfzo 
 |-  ..^
9 chash 
 |-  #
10 3 9 cfv 
 |-  ( # ` w )
11 cmin 
 |-  -
12 c1 
 |-  1
13 10 12 11 co 
 |-  ( ( # ` w ) - 1 )
14 7 13 8 co 
 |-  ( 0 ..^ ( ( # ` w ) - 1 ) )
15 6 cv 
 |-  k
16 15 3 cfv 
 |-  ( w ` k )
17 clt 
 |-  <
18 caddc 
 |-  +
19 15 12 18 co 
 |-  ( k + 1 )
20 19 3 cfv 
 |-  ( w ` ( k + 1 ) )
21 16 20 17 wbr 
 |-  ( w ` k ) < ( w ` ( k + 1 ) )
22 21 6 14 wral 
 |-  A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) )
23 5 22 wa 
 |-  ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) )
24 23 2 cab 
 |-  { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) }
25 1 24 wceq 
 |-  UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) }