Step | Hyp | Ref
| Expression |
1 | | csplice 14698 |
. 2
class
splice |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vb |
. . 3
setvar 𝑏 |
4 | | cvv 3474 |
. . 3
class
V |
5 | 2 | cv 1540 |
. . . . . 6
class 𝑠 |
6 | 3 | cv 1540 |
. . . . . . . 8
class 𝑏 |
7 | | c1st 7972 |
. . . . . . . 8
class
1st |
8 | 6, 7 | cfv 6543 |
. . . . . . 7
class
(1st ‘𝑏) |
9 | 8, 7 | cfv 6543 |
. . . . . 6
class
(1st ‘(1st ‘𝑏)) |
10 | | cpfx 14619 |
. . . . . 6
class
prefix |
11 | 5, 9, 10 | co 7408 |
. . . . 5
class (𝑠 prefix (1st
‘(1st ‘𝑏))) |
12 | | c2nd 7973 |
. . . . . 6
class
2nd |
13 | 6, 12 | cfv 6543 |
. . . . 5
class
(2nd ‘𝑏) |
14 | | cconcat 14519 |
. . . . 5
class
++ |
15 | 11, 13, 14 | co 7408 |
. . . 4
class ((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) |
16 | 8, 12 | cfv 6543 |
. . . . . 6
class
(2nd ‘(1st ‘𝑏)) |
17 | | chash 14289 |
. . . . . . 7
class
♯ |
18 | 5, 17 | cfv 6543 |
. . . . . 6
class
(♯‘𝑠) |
19 | 16, 18 | cop 4634 |
. . . . 5
class
⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩ |
20 | | csubstr 14589 |
. . . . 5
class
substr |
21 | 5, 19, 20 | co 7408 |
. . . 4
class (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩) |
22 | 15, 21, 14 | co 7408 |
. . 3
class (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩)) |
23 | 2, 3, 4, 4, 22 | cmpo 7410 |
. 2
class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩))) |
24 | 1, 23 | wceq 1541 |
1
wff splice =
(𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩))) |