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 = ( 𝑠 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ↦ ( 𝑠 ‘ ( ( ( ♯ ‘ 𝑠 ) − 1 ) − 𝑥 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creverse	⊢ reverse
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cc0	⊢ 0
5		cfzo	⊢ ..^
6		chash	⊢ ♯
7	1	cv	⊢ 𝑠
8	7 6	cfv	⊢ ( ♯ ‘ 𝑠 )
9	4 8 5	co	⊢ ( 0 ..^ ( ♯ ‘ 𝑠 ) )
10		cmin	⊢ −
11		c1	⊢ 1
12	8 11 10	co	⊢ ( ( ♯ ‘ 𝑠 ) − 1 )
13	3	cv	⊢ 𝑥
14	12 13 10	co	⊢ ( ( ( ♯ ‘ 𝑠 ) − 1 ) − 𝑥 )
15	14 7	cfv	⊢ ( 𝑠 ‘ ( ( ( ♯ ‘ 𝑠 ) − 1 ) − 𝑥 ) )
16	3 9 15	cmpt	⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ↦ ( 𝑠 ‘ ( ( ( ♯ ‘ 𝑠 ) − 1 ) − 𝑥 ) ) )
17	1 2 16	cmpt	⊢ ( 𝑠 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ↦ ( 𝑠 ‘ ( ( ( ♯ ‘ 𝑠 ) − 1 ) − 𝑥 ) ) ) )
18	0 17	wceq	⊢ reverse = ( 𝑠 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ↦ ( 𝑠 ‘ ( ( ( ♯ ‘ 𝑠 ) − 1 ) − 𝑥 ) ) ) )