Metamath Proof Explorer


Definition df-reverse

Description: Define an operation which reverses the order of symbols in a word. This operation is also known as "word reversal" and "word mirroring". (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion df-reverse
|- reverse = ( s e. _V |-> ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 creverse
 |-  reverse
1 vs
 |-  s
2 cvv
 |-  _V
3 vx
 |-  x
4 cc0
 |-  0
5 cfzo
 |-  ..^
6 chash
 |-  #
7 1 cv
 |-  s
8 7 6 cfv
 |-  ( # ` s )
9 4 8 5 co
 |-  ( 0 ..^ ( # ` s ) )
10 cmin
 |-  -
11 c1
 |-  1
12 8 11 10 co
 |-  ( ( # ` s ) - 1 )
13 3 cv
 |-  x
14 12 13 10 co
 |-  ( ( ( # ` s ) - 1 ) - x )
15 14 7 cfv
 |-  ( s ` ( ( ( # ` s ) - 1 ) - x ) )
16 3 9 15 cmpt
 |-  ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) )
17 1 2 16 cmpt
 |-  ( s e. _V |-> ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) )
18 0 17 wceq
 |-  reverse = ( s e. _V |-> ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) )