Definition df-concat 14126

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 14125	. 2 class ++
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cvv 3408	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6		cc0 10729	. . . . 5 class 0
7	2	cv 1542	. . . . . . 7 class 𝑠
8		chash 13896	. . . . . . 7 class ♯
9	7, 8	cfv 6380	. . . . . 6 class (♯‘𝑠)
10	3	cv 1542	. . . . . . 7 class 𝑡
11	10, 8	cfv 6380	. . . . . 6 class (♯‘𝑡)
12		caddc 10732	. . . . . 6 class +
13	9, 11, 12	co 7213	. . . . 5 class ((♯‘𝑠) + (♯‘𝑡))
14		cfzo 13238	. . . . 5 class ..^
15	6, 13, 14	co 7213	. . . 4 class (0..^((♯‘𝑠) + (♯‘𝑡)))
16	5	cv 1542	. . . . . 6 class 𝑥
17	6, 9, 14	co 7213	. . . . . 6 class (0..^(♯‘𝑠))
18	16, 17	wcel 2110	. . . . 5 wff 𝑥 ∈ (0..^(♯‘𝑠))
19	16, 7	cfv 6380	. . . . 5 class (𝑠‘𝑥)
20		cmin 11062	. . . . . . 7 class −
21	16, 9, 20	co 7213	. . . . . 6 class (𝑥 − (♯‘𝑠))
22	21, 10	cfv 6380	. . . . 5 class (𝑡‘(𝑥 − (♯‘𝑠)))
23	18, 19, 22	cif 4439	. . . 4 class if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))
24	5, 15, 23	cmpt 5135	. . 3 class (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠)))))
25	2, 3, 4, 4, 24	cmpo 7215	. 2 class (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
26	1, 25	wceq 1543	1 wff ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))

This definition is referenced by:  ccatfn  14127  ccatfval  14128