Detailed syntax breakdown of Definition df-concat
Step | Hyp | Ref
| Expression |
1 | | cconcat 13148 |
. 2
class
++ |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vt |
. . 3
setvar 𝑡 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | | cc0 9815 |
. . . . 5
class
0 |
7 | 2 | cv 1474 |
. . . . . . 7
class 𝑠 |
8 | | chash 12979 |
. . . . . . 7
class
# |
9 | 7, 8 | cfv 5804 |
. . . . . 6
class
(#‘𝑠) |
10 | 3 | cv 1474 |
. . . . . . 7
class 𝑡 |
11 | 10, 8 | cfv 5804 |
. . . . . 6
class
(#‘𝑡) |
12 | | caddc 9818 |
. . . . . 6
class
+ |
13 | 9, 11, 12 | co 6549 |
. . . . 5
class
((#‘𝑠) +
(#‘𝑡)) |
14 | | cfzo 12334 |
. . . . 5
class
..^ |
15 | 6, 13, 14 | co 6549 |
. . . 4
class
(0..^((#‘𝑠) +
(#‘𝑡))) |
16 | 5 | cv 1474 |
. . . . . 6
class 𝑥 |
17 | 6, 9, 14 | co 6549 |
. . . . . 6
class
(0..^(#‘𝑠)) |
18 | 16, 17 | wcel 1977 |
. . . . 5
wff 𝑥 ∈ (0..^(#‘𝑠)) |
19 | 16, 7 | cfv 5804 |
. . . . 5
class (𝑠‘𝑥) |
20 | | cmin 10145 |
. . . . . . 7
class
− |
21 | 16, 9, 20 | co 6549 |
. . . . . 6
class (𝑥 − (#‘𝑠)) |
22 | 21, 10 | cfv 5804 |
. . . . 5
class (𝑡‘(𝑥 − (#‘𝑠))) |
23 | 18, 19, 22 | cif 4036 |
. . . 4
class if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))) |
24 | 5, 15, 23 | cmpt 4643 |
. . 3
class (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠))))) |
25 | 2, 3, 4, 4, 24 | cmpt2 6551 |
. 2
class (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))))) |
26 | 1, 25 | wceq 1475 |
1
wff ++ =
(𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))))) |