This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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