Detailed syntax breakdown of Definition df-splice
Step | Hyp | Ref
| Expression |
1 | | csplice 13296 |
. 2
class
splice |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vb |
. . 3
setvar 𝑏 |
4 | | cvv 3200 |
. . 3
class
V |
5 | 2 | cv 1482 |
. . . . . 6
class 𝑠 |
6 | | cc0 9936 |
. . . . . . 7
class
0 |
7 | 3 | cv 1482 |
. . . . . . . . 9
class 𝑏 |
8 | | c1st 7166 |
. . . . . . . . 9
class
1st |
9 | 7, 8 | cfv 5888 |
. . . . . . . 8
class
(1st ‘𝑏) |
10 | 9, 8 | cfv 5888 |
. . . . . . 7
class
(1st ‘(1st ‘𝑏)) |
11 | 6, 10 | cop 4183 |
. . . . . 6
class 〈0,
(1st ‘(1st ‘𝑏))〉 |
12 | | csubstr 13295 |
. . . . . 6
class
substr |
13 | 5, 11, 12 | co 6650 |
. . . . 5
class (𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) |
14 | | c2nd 7167 |
. . . . . 6
class
2nd |
15 | 7, 14 | cfv 5888 |
. . . . 5
class
(2nd ‘𝑏) |
16 | | cconcat 13293 |
. . . . 5
class
++ |
17 | 13, 15, 16 | co 6650 |
. . . 4
class ((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) |
18 | 9, 14 | cfv 5888 |
. . . . . 6
class
(2nd ‘(1st ‘𝑏)) |
19 | | chash 13117 |
. . . . . . 7
class
# |
20 | 5, 19 | cfv 5888 |
. . . . . 6
class
(#‘𝑠) |
21 | 18, 20 | cop 4183 |
. . . . 5
class
〈(2nd ‘(1st ‘𝑏)), (#‘𝑠)〉 |
22 | 5, 21, 12 | co 6650 |
. . . 4
class (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉) |
23 | 17, 22, 16 | co 6650 |
. . 3
class (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉)) |
24 | 2, 3, 4, 4, 23 | cmpt2 6652 |
. 2
class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉))) |
25 | 1, 24 | wceq 1483 |
1
wff splice =
(𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉))) |