Detailed syntax breakdown of Definition df-itg2
Step | Hyp | Ref
| Expression |
1 | | citg2 23191 |
. 2
class
∫2 |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | cc0 9815 |
. . . . 5
class
0 |
4 | | cpnf 9950 |
. . . . 5
class
+∞ |
5 | | cicc 12049 |
. . . . 5
class
[,] |
6 | 3, 4, 5 | co 6549 |
. . . 4
class
(0[,]+∞) |
7 | | cr 9814 |
. . . 4
class
ℝ |
8 | | cmap 7744 |
. . . 4
class
↑𝑚 |
9 | 6, 7, 8 | co 6549 |
. . 3
class
((0[,]+∞) ↑𝑚 ℝ) |
10 | | vg |
. . . . . . . . 9
setvar 𝑔 |
11 | 10 | cv 1474 |
. . . . . . . 8
class 𝑔 |
12 | 2 | cv 1474 |
. . . . . . . 8
class 𝑓 |
13 | | cle 9954 |
. . . . . . . . 9
class
≤ |
14 | 13 | cofr 6794 |
. . . . . . . 8
class
∘𝑟 ≤ |
15 | 11, 12, 14 | wbr 4583 |
. . . . . . 7
wff 𝑔 ∘𝑟
≤ 𝑓 |
16 | | vx |
. . . . . . . . 9
setvar 𝑥 |
17 | 16 | cv 1474 |
. . . . . . . 8
class 𝑥 |
18 | | citg1 23190 |
. . . . . . . . 9
class
∫1 |
19 | 11, 18 | cfv 5804 |
. . . . . . . 8
class
(∫1‘𝑔) |
20 | 17, 19 | wceq 1475 |
. . . . . . 7
wff 𝑥 =
(∫1‘𝑔) |
21 | 15, 20 | wa 383 |
. . . . . 6
wff (𝑔 ∘𝑟
≤ 𝑓 ∧ 𝑥 =
(∫1‘𝑔)) |
22 | 18 | cdm 5038 |
. . . . . 6
class dom
∫1 |
23 | 21, 10, 22 | wrex 2897 |
. . . . 5
wff
∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔)) |
24 | 23, 16 | cab 2596 |
. . . 4
class {𝑥 ∣ ∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))} |
25 | | cxr 9952 |
. . . 4
class
ℝ* |
26 | | clt 9953 |
. . . 4
class
< |
27 | 24, 25, 26 | csup 8229 |
. . 3
class
sup({𝑥 ∣
∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, <
) |
28 | 2, 9, 27 | cmpt 4643 |
. 2
class (𝑓 ∈ ((0[,]+∞)
↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ 𝑓 ∧ 𝑥 =
(∫1‘𝑔))}, ℝ*, <
)) |
29 | 1, 28 | wceq 1475 |
1
wff
∫2 = (𝑓 ∈ ((0[,]+∞)
↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ 𝑓 ∧ 𝑥 =
(∫1‘𝑔))}, ℝ*, <
)) |