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..^(♯‘𝑠)),
(𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠)))))) |