Definition df-concat 14716

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 14715	. 2 class ++
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cvv 3451	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6		cc0 11200	. . . . 5 class 0
7	2	cv 1569	. . . . . . 7 class 𝑠
8		chash 14474	. . . . . . 7 class ♯
9	7, 8	cfv 6538	. . . . . 6 class (♯‘𝑠)
10	3	cv 1569	. . . . . . 7 class 𝑡
11	10, 8	cfv 6538	. . . . . 6 class (♯‘𝑡)
12		caddc 11203	. . . . . 6 class +
13	9, 11, 12	co 7420	. . . . 5 class ((♯‘𝑠) + (♯‘𝑡))
14		cfzo 13788	. . . . 5 class ..^
15	6, 13, 14	co 7420	. . . 4 class (0..^((♯‘𝑠) + (♯‘𝑡)))
16	5	cv 1569	. . . . . 6 class 𝑥
17	6, 9, 14	co 7420	. . . . . 6 class (0..^(♯‘𝑠))
18	16, 17	wcel 2145	. . . . 5 wff 𝑥 ∈ (0..^(♯‘𝑠))
19	16, 7	cfv 6538	. . . . 5 class (𝑠‘𝑥)
20		cmin 11541	. . . . . . 7 class −
21	16, 9, 20	co 7420	. . . . . 6 class (𝑥 − (♯‘𝑠))
22	21, 10	cfv 6538	. . . . 5 class (𝑡‘(𝑥 − (♯‘𝑠)))
23	18, 19, 22	cif 4482	. . . 4 class if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))
24	5, 15, 23	cmpt 5186	. . 3 class (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠)))))
25	2, 3, 4, 4, 24	cmpo 7422	. 2 class (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
26	1, 25	wceq 1570	1 wff ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))

This definition is used by:  ccatfn  14717  ccatfval  14718