Detailed syntax breakdown of Definition df-o1
| Step | Hyp | Ref
| Expression |
| 1 | | co1 15522 |
. 2
class
𝑂(1) |
| 2 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
| 3 | 2 | cv 1539 |
. . . . . . . . 9
class 𝑦 |
| 4 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
| 5 | 4 | cv 1539 |
. . . . . . . . 9
class 𝑓 |
| 6 | 3, 5 | cfv 6561 |
. . . . . . . 8
class (𝑓‘𝑦) |
| 7 | | cabs 15273 |
. . . . . . . 8
class
abs |
| 8 | 6, 7 | cfv 6561 |
. . . . . . 7
class
(abs‘(𝑓‘𝑦)) |
| 9 | | vm |
. . . . . . . 8
setvar 𝑚 |
| 10 | 9 | cv 1539 |
. . . . . . 7
class 𝑚 |
| 11 | | cle 11296 |
. . . . . . 7
class
≤ |
| 12 | 8, 10, 11 | wbr 5143 |
. . . . . 6
wff
(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
| 13 | 5 | cdm 5685 |
. . . . . . 7
class dom 𝑓 |
| 14 | | vx |
. . . . . . . . 9
setvar 𝑥 |
| 15 | 14 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 16 | | cpnf 11292 |
. . . . . . . 8
class
+∞ |
| 17 | | cico 13389 |
. . . . . . . 8
class
[,) |
| 18 | 15, 16, 17 | co 7431 |
. . . . . . 7
class (𝑥[,)+∞) |
| 19 | 13, 18 | cin 3950 |
. . . . . 6
class (dom
𝑓 ∩ (𝑥[,)+∞)) |
| 20 | 12, 2, 19 | wral 3061 |
. . . . 5
wff
∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
| 21 | | cr 11154 |
. . . . 5
class
ℝ |
| 22 | 20, 9, 21 | wrex 3070 |
. . . 4
wff
∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
| 23 | 22, 14, 21 | wrex 3070 |
. . 3
wff
∃𝑥 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
| 24 | | cc 11153 |
. . . 4
class
ℂ |
| 25 | | cpm 8867 |
. . . 4
class
↑pm |
| 26 | 24, 21, 25 | co 7431 |
. . 3
class (ℂ
↑pm ℝ) |
| 27 | 23, 4, 26 | crab 3436 |
. 2
class {𝑓 ∈ (ℂ
↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚} |
| 28 | 1, 27 | wceq 1540 |
1
wff
𝑂(1) = {𝑓
∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚} |