This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Words over a set Reversing words 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 ∈ V ⟼ x ∈ 0 ..^ s ⟼ s s - 1 - x
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
creverse class reverse
1
vs setvar s
2
cvv class V
3
vx setvar x
4
cc0 class 0
5
cfzo class ..^
6
chash class .
7
1
cv setvar s
8
7 6
cfv class s
9
4 8 5
co class 0 ..^ s
10
cmin class −
11
c1 class 1
12
8 11 10
co class s − 1
13
3
cv setvar x
14
12 13 10
co class s - 1 - x
15
14 7
cfv class s s - 1 - x
16
3 9 15
cmpt class x ∈ 0 ..^ s ⟼ s s - 1 - x
17
1 2 16
cmpt class s ∈ V ⟼ x ∈ 0 ..^ s ⟼ s s - 1 - x
18
0 17
wceq wff reverse = s ∈ V ⟼ x ∈ 0 ..^ s ⟼ s s - 1 - x