Detailed syntax breakdown of Definition df-concat
Step | Hyp | Ref
| Expression |
1 | | cconcat 13293 |
. 2
class
++ |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vt |
. . 3
setvar 𝑡 |
4 | | cvv 3200 |
. . 3
class
V |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | | cc0 9936 |
. . . . 5
class
0 |
7 | 2 | cv 1482 |
. . . . . . 7
class 𝑠 |
8 | | chash 13117 |
. . . . . . 7
class
# |
9 | 7, 8 | cfv 5888 |
. . . . . 6
class
(#‘𝑠) |
10 | 3 | cv 1482 |
. . . . . . 7
class 𝑡 |
11 | 10, 8 | cfv 5888 |
. . . . . 6
class
(#‘𝑡) |
12 | | caddc 9939 |
. . . . . 6
class
+ |
13 | 9, 11, 12 | co 6650 |
. . . . 5
class
((#‘𝑠) +
(#‘𝑡)) |
14 | | cfzo 12465 |
. . . . 5
class
..^ |
15 | 6, 13, 14 | co 6650 |
. . . 4
class
(0..^((#‘𝑠) +
(#‘𝑡))) |
16 | 5 | cv 1482 |
. . . . . 6
class 𝑥 |
17 | 6, 9, 14 | co 6650 |
. . . . . 6
class
(0..^(#‘𝑠)) |
18 | 16, 17 | wcel 1990 |
. . . . 5
wff 𝑥 ∈ (0..^(#‘𝑠)) |
19 | 16, 7 | cfv 5888 |
. . . . 5
class (𝑠‘𝑥) |
20 | | cmin 10266 |
. . . . . . 7
class
− |
21 | 16, 9, 20 | co 6650 |
. . . . . 6
class (𝑥 − (#‘𝑠)) |
22 | 21, 10 | cfv 5888 |
. . . . 5
class (𝑡‘(𝑥 − (#‘𝑠))) |
23 | 18, 19, 22 | cif 4086 |
. . . 4
class if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))) |
24 | 5, 15, 23 | cmpt 4729 |
. . 3
class (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠))))) |
25 | 2, 3, 4, 4, 24 | cmpt2 6652 |
. 2
class (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))))) |
26 | 1, 25 | wceq 1483 |
1
wff ++ =
(𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))))) |