Definition df-spliceOLD 13888

Description: Obsolete version of df-splice 13887 as of 12-Oct-2022. Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (New usage is discouraged.)

Assertion

Ref	Expression
df-spliceOLD	⊢ spliceOLD = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)))

Distinct variable group:   𝑠,𝑏

Detailed syntax breakdown of Definition df-spliceOLD

Step	Hyp	Ref	Expression
1		cspliceOLD 13886	. 2 class spliceOLD
2		vs	. . 3 setvar 𝑠
3		vb	. . 3 setvar 𝑏
4		cvv 3397	. . 3 class V
5	2	cv 1600	. . . . . 6 class 𝑠
6		cc0 10272	. . . . . . 7 class 0
7	3	cv 1600	. . . . . . . . 9 class 𝑏
8		c1st 7443	. . . . . . . . 9 class 1st
9	7, 8	cfv 6135	. . . . . . . 8 class (1st ‘𝑏)
10	9, 8	cfv 6135	. . . . . . 7 class (1st ‘(1st ‘𝑏))
11	6, 10	cop 4403	. . . . . 6 class ⟨0, (1st ‘(1st ‘𝑏))⟩
12		csubstr 13730	. . . . . 6 class substr
13	5, 11, 12	co 6922	. . . . 5 class (𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩)
14		c2nd 7444	. . . . . 6 class 2nd
15	7, 14	cfv 6135	. . . . 5 class (2nd ‘𝑏)
16		cconcat 13660	. . . . 5 class ++
17	13, 15, 16	co 6922	. . . 4 class ((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏))
18	9, 14	cfv 6135	. . . . . 6 class (2nd ‘(1st ‘𝑏))
19		chash 13435	. . . . . . 7 class ♯
20	5, 19	cfv 6135	. . . . . 6 class (♯‘𝑠)
21	18, 20	cop 4403	. . . . 5 class ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩
22	5, 21, 12	co 6922	. . . 4 class (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)
23	17, 22, 16	co 6922	. . 3 class (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩))
24	2, 3, 4, 4, 23	cmpt2 6924	. 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)))
25	1, 24	wceq 1601	1 wff spliceOLD = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)))

This definition is referenced by:  splvalpfxOLD  13889  splvalOLD  13891  splclOLD  13893