Definition df-reverse 13305

Description: Define an operation which reverses the order of symbols in a word. (Contributed by Stefan O'Rear, 26-Aug-2015.)

Assertion

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

Distinct variable group:   x, s

Detailed syntax breakdown of Definition df-reverse

Step	Hyp	Ref	Expression
1		creverse 13297	. 2 class reverse
2		vs	. . 3 setvar s
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5		cc0 9936	. . . . 5 class 0
6	2	cv 1482	. . . . . 6 class s
7		chash 13117	. . . . . 6 class #
8	6, 7	cfv 5888	. . . . 5 class ( # ` s )
9		cfzo 12465	. . . . 5 class ..^
10	5, 8, 9	co 6650	. . . 4 class ( 0..^ ( # ` s ) )
11		c1 9937	. . . . . . 7 class 1
12		cmin 10266	. . . . . . 7 class -
13	8, 11, 12	co 6650	. . . . . 6 class ( ( # ` s ) - 1 )
14	4	cv 1482	. . . . . 6 class x
15	13, 14, 12	co 6650	. . . . 5 class ( ( ( # ` s ) - 1 ) - x )
16	15, 6	cfv 5888	. . . 4 class ( s ` ( ( ( # ` s ) - 1 ) - x ) )
17	4, 10, 16	cmpt 4729	. . 3 class ( x e. ( 0..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) )
18	2, 3, 17	cmpt 4729	. 2 class ( s e. _V |-> ( x e. ( 0..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) )
19	1, 18	wceq 1483	1 wff reverse = ( s e. _V |-> ( x e. ( 0..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) )

This definition is referenced by:  revval  13509