MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-reverse Structured version   Visualization version   GIF version

Definition df-reverse 14461
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
StepHypRef Expression
1 creverse 14460 . 2 class reverse
2 vs . . 3 setvar 𝑠
3 cvv 3431 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 cc0 10860 . . . . 5 class 0
62cv 1538 . . . . . 6 class 𝑠
7 chash 14033 . . . . . 6 class
86, 7cfv 6428 . . . . 5 class (♯‘𝑠)
9 cfzo 13371 . . . . 5 class ..^
105, 8, 9co 7269 . . . 4 class (0..^(♯‘𝑠))
11 c1 10861 . . . . . . 7 class 1
12 cmin 11194 . . . . . . 7 class
138, 11, 12co 7269 . . . . . 6 class ((♯‘𝑠) − 1)
144cv 1538 . . . . . 6 class 𝑥
1513, 14, 12co 7269 . . . . 5 class (((♯‘𝑠) − 1) − 𝑥)
1615, 6cfv 6428 . . . 4 class (𝑠‘(((♯‘𝑠) − 1) − 𝑥))
174, 10, 16cmpt 5158 . . 3 class (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥)))
182, 3, 17cmpt 5158 . 2 class (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))))
191, 18wceq 1539 1 wff reverse = (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  revval  14462
  Copyright terms: Public domain W3C validator