Detailed syntax breakdown of Definition df-iccp
Step | Hyp | Ref
| Expression |
1 | | ciccp 44419 |
. 2
class
RePart |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | cn 11716 |
. . 3
class
ℕ |
4 | | vi |
. . . . . . . 8
setvar 𝑖 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑖 |
6 | | vp |
. . . . . . . 8
setvar 𝑝 |
7 | 6 | cv 1541 |
. . . . . . 7
class 𝑝 |
8 | 5, 7 | cfv 6339 |
. . . . . 6
class (𝑝‘𝑖) |
9 | | c1 10616 |
. . . . . . . 8
class
1 |
10 | | caddc 10618 |
. . . . . . . 8
class
+ |
11 | 5, 9, 10 | co 7170 |
. . . . . . 7
class (𝑖 + 1) |
12 | 11, 7 | cfv 6339 |
. . . . . 6
class (𝑝‘(𝑖 + 1)) |
13 | | clt 10753 |
. . . . . 6
class
< |
14 | 8, 12, 13 | wbr 5030 |
. . . . 5
wff (𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) |
15 | | cc0 10615 |
. . . . . 6
class
0 |
16 | 2 | cv 1541 |
. . . . . 6
class 𝑚 |
17 | | cfzo 13124 |
. . . . . 6
class
..^ |
18 | 15, 16, 17 | co 7170 |
. . . . 5
class
(0..^𝑚) |
19 | 14, 4, 18 | wral 3053 |
. . . 4
wff
∀𝑖 ∈
(0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) |
20 | | cxr 10752 |
. . . . 5
class
ℝ* |
21 | | cfz 12981 |
. . . . . 6
class
... |
22 | 15, 16, 21 | co 7170 |
. . . . 5
class
(0...𝑚) |
23 | | cmap 8437 |
. . . . 5
class
↑m |
24 | 20, 22, 23 | co 7170 |
. . . 4
class
(ℝ* ↑m (0...𝑚)) |
25 | 19, 6, 24 | crab 3057 |
. . 3
class {𝑝 ∈ (ℝ*
↑m (0...𝑚))
∣ ∀𝑖 ∈
(0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))} |
26 | 2, 3, 25 | cmpt 5110 |
. 2
class (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ*
↑m (0...𝑚))
∣ ∀𝑖 ∈
(0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) |
27 | 1, 26 | wceq 1542 |
1
wff RePart =
(𝑚 ∈ ℕ ↦
{𝑝 ∈
(ℝ* ↑m (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) |