Detailed syntax breakdown of Definition df-reverse
Step | Hyp | Ref
| 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 |
6 | 2 | cv 1538 |
. . . . . 6
class 𝑠 |
7 | | chash 14033 |
. . . . . 6
class
♯ |
8 | 6, 7 | cfv 6428 |
. . . . 5
class
(♯‘𝑠) |
9 | | cfzo 13371 |
. . . . 5
class
..^ |
10 | 5, 8, 9 | co 7269 |
. . . 4
class
(0..^(♯‘𝑠)) |
11 | | c1 10861 |
. . . . . . 7
class
1 |
12 | | cmin 11194 |
. . . . . . 7
class
− |
13 | 8, 11, 12 | co 7269 |
. . . . . 6
class
((♯‘𝑠)
− 1) |
14 | 4 | cv 1538 |
. . . . . 6
class 𝑥 |
15 | 13, 14, 12 | co 7269 |
. . . . 5
class
(((♯‘𝑠)
− 1) − 𝑥) |
16 | 15, 6 | cfv 6428 |
. . . 4
class (𝑠‘(((♯‘𝑠) − 1) − 𝑥)) |
17 | 4, 10, 16 | cmpt 5158 |
. . 3
class (𝑥 ∈
(0..^(♯‘𝑠))
↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))) |
18 | 2, 3, 17 | cmpt 5158 |
. 2
class (𝑠 ∈ V ↦ (𝑥 ∈
(0..^(♯‘𝑠))
↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥)))) |
19 | 1, 18 | wceq 1539 |
1
wff reverse =
(𝑠 ∈ V ↦ (𝑥 ∈
(0..^(♯‘𝑠))
↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥)))) |