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	$$⊢\mathrm{reverse}=\left(s\in \mathrm{V}⟼\left(x\in \left(0..^\left|s\right|\right)⟼s\left(\left|s\right|-1-x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creverse	$$class\mathrm{reverse}$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cc0	$$class0$$
5		cfzo	$$class..^$$
6		chash	$$class\left|.\right|$$
7	1	cv	$$setvars$$
8	7 6	cfv	$$class\left|s\right|$$
9	4 8 5	co	$$class\left(0..^\left|s\right|\right)$$
10		cmin	$$class-$$
11		c1	$$class1$$
12	8 11 10	co	$$class\left(\left|s\right|-1\right)$$
13	3	cv	$$setvarx$$
14	12 13 10	co	$$class\left(\left|s\right|-1-x\right)$$
15	14 7	cfv	$$classs\left(\left|s\right|-1-x\right)$$
16	3 9 15	cmpt	$$class\left(x\in \left(0..^\left|s\right|\right)⟼s\left(\left|s\right|-1-x\right)\right)$$
17	1 2 16	cmpt	$$class\left(s\in \mathrm{V}⟼\left(x\in \left(0..^\left|s\right|\right)⟼s\left(\left|s\right|-1-x\right)\right)\right)$$
18	0 17	wceq	$$wff\mathrm{reverse}=\left(s\in \mathrm{V}⟼\left(x\in \left(0..^\left|s\right|\right)⟼s\left(\left|s\right|-1-x\right)\right)\right)$$