Definition df-concat 14594

Description: Define the concatenation operator which combines two words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)

Assertion

Ref	Expression
df-concat	⊢ ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))

Distinct variable group:   𝑡,𝑠,𝑥

Detailed syntax breakdown of Definition df-concat

Step	Hyp	Ref	Expression
1		cconcat 14593	. 2 class ++
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cvv 3464	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6		cc0 11134	. . . . 5 class 0
7	2	cv 1539	. . . . . . 7 class 𝑠
8		chash 14353	. . . . . . 7 class ♯
9	7, 8	cfv 6536	. . . . . 6 class (♯‘𝑠)
10	3	cv 1539	. . . . . . 7 class 𝑡
11	10, 8	cfv 6536	. . . . . 6 class (♯‘𝑡)
12		caddc 11137	. . . . . 6 class +
13	9, 11, 12	co 7410	. . . . 5 class ((♯‘𝑠) + (♯‘𝑡))
14		cfzo 13676	. . . . 5 class ..^
15	6, 13, 14	co 7410	. . . 4 class (0..^((♯‘𝑠) + (♯‘𝑡)))
16	5	cv 1539	. . . . . 6 class 𝑥
17	6, 9, 14	co 7410	. . . . . 6 class (0..^(♯‘𝑠))
18	16, 17	wcel 2109	. . . . 5 wff 𝑥 ∈ (0..^(♯‘𝑠))
19	16, 7	cfv 6536	. . . . 5 class (𝑠‘𝑥)
20		cmin 11471	. . . . . . 7 class −
21	16, 9, 20	co 7410	. . . . . 6 class (𝑥 − (♯‘𝑠))
22	21, 10	cfv 6536	. . . . 5 class (𝑡‘(𝑥 − (♯‘𝑠)))
23	18, 19, 22	cif 4505	. . . 4 class if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))
24	5, 15, 23	cmpt 5206	. . 3 class (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠)))))
25	2, 3, 4, 4, 24	cmpo 7412	. 2 class (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
26	1, 25	wceq 1540	1 wff ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))

This definition is referenced by:  ccatfn  14595  ccatfval  14596