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 ) ) ) )