Detailed syntax breakdown of Definition df-ovol
Step | Hyp | Ref
| Expression |
1 | | covol 24313 |
. 2
class
vol* |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cr 10693 |
. . . 4
class
ℝ |
4 | 3 | cpw 4499 |
. . 3
class 𝒫
ℝ |
5 | 2 | cv 1542 |
. . . . . . . 8
class 𝑥 |
6 | | cioo 12900 |
. . . . . . . . . . 11
class
(,) |
7 | | vf |
. . . . . . . . . . . 12
setvar 𝑓 |
8 | 7 | cv 1542 |
. . . . . . . . . . 11
class 𝑓 |
9 | 6, 8 | ccom 5540 |
. . . . . . . . . 10
class ((,)
∘ 𝑓) |
10 | 9 | crn 5537 |
. . . . . . . . 9
class ran ((,)
∘ 𝑓) |
11 | 10 | cuni 4805 |
. . . . . . . 8
class ∪ ran ((,) ∘ 𝑓) |
12 | 5, 11 | wss 3853 |
. . . . . . 7
wff 𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) |
13 | | vy |
. . . . . . . . 9
setvar 𝑦 |
14 | 13 | cv 1542 |
. . . . . . . 8
class 𝑦 |
15 | | caddc 10697 |
. . . . . . . . . . 11
class
+ |
16 | | cabs 14762 |
. . . . . . . . . . . . 13
class
abs |
17 | | cmin 11027 |
. . . . . . . . . . . . 13
class
− |
18 | 16, 17 | ccom 5540 |
. . . . . . . . . . . 12
class (abs
∘ − ) |
19 | 18, 8 | ccom 5540 |
. . . . . . . . . . 11
class ((abs
∘ − ) ∘ 𝑓) |
20 | | c1 10695 |
. . . . . . . . . . 11
class
1 |
21 | 15, 19, 20 | cseq 13539 |
. . . . . . . . . 10
class seq1( + ,
((abs ∘ − ) ∘ 𝑓)) |
22 | 21 | crn 5537 |
. . . . . . . . 9
class ran seq1(
+ , ((abs ∘ − ) ∘ 𝑓)) |
23 | | cxr 10831 |
. . . . . . . . 9
class
ℝ* |
24 | | clt 10832 |
. . . . . . . . 9
class
< |
25 | 22, 23, 24 | csup 9034 |
. . . . . . . 8
class sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
) |
26 | 14, 25 | wceq 1543 |
. . . . . . 7
wff 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
) |
27 | 12, 26 | wa 399 |
. . . . . 6
wff (𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) |
28 | | cle 10833 |
. . . . . . . 8
class
≤ |
29 | 3, 3 | cxp 5534 |
. . . . . . . 8
class (ℝ
× ℝ) |
30 | 28, 29 | cin 3852 |
. . . . . . 7
class ( ≤
∩ (ℝ × ℝ)) |
31 | | cn 11795 |
. . . . . . 7
class
ℕ |
32 | | cmap 8486 |
. . . . . . 7
class
↑m |
33 | 30, 31, 32 | co 7191 |
. . . . . 6
class (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) |
34 | 27, 7, 33 | wrex 3052 |
. . . . 5
wff
∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) |
35 | 34, 13, 23 | crab 3055 |
. . . 4
class {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
36 | 35, 23, 24 | cinf 9035 |
. . 3
class
inf({𝑦 ∈
ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))},
ℝ*, < ) |
37 | 2, 4, 36 | cmpt 5120 |
. 2
class (𝑥 ∈ 𝒫 ℝ
↦ inf({𝑦 ∈
ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))},
ℝ*, < )) |
38 | 1, 37 | wceq 1543 |
1
wff vol* =
(𝑥 ∈ 𝒫 ℝ
↦ inf({𝑦 ∈
ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))},
ℝ*, < )) |