Definition df-reverse 14400

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

Assertion

Ref	Expression
df-reverse	⊢ reverse = (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))))

Distinct variable group:   𝑥,𝑠

Detailed syntax breakdown of Definition df-reverse

Step	Hyp	Ref	Expression
1		creverse 14399	. 2 class reverse
2		vs	. . 3 setvar 𝑠
3		cvv 3422	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		cc0 10802	. . . . 5 class 0
6	2	cv 1538	. . . . . 6 class 𝑠
7		chash 13972	. . . . . 6 class ♯
8	6, 7	cfv 6418	. . . . 5 class (♯‘𝑠)
9		cfzo 13311	. . . . 5 class ..^
10	5, 8, 9	co 7255	. . . 4 class (0..^(♯‘𝑠))
11		c1 10803	. . . . . . 7 class 1
12		cmin 11135	. . . . . . 7 class −
13	8, 11, 12	co 7255	. . . . . 6 class ((♯‘𝑠) − 1)
14	4	cv 1538	. . . . . 6 class 𝑥
15	13, 14, 12	co 7255	. . . . 5 class (((♯‘𝑠) − 1) − 𝑥)
16	15, 6	cfv 6418	. . . 4 class (𝑠‘(((♯‘𝑠) − 1) − 𝑥))
17	4, 10, 16	cmpt 5153	. . 3 class (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥)))
18	2, 3, 17	cmpt 5153	. 2 class (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))))
19	1, 18	wceq 1539	1 wff reverse = (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))))

This definition is referenced by:  revval  14401