Detailed syntax breakdown of Definition df-o1
Step | Hyp | Ref
| Expression |
1 | | co1 14933 |
. 2
class
𝑂(1) |
2 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
3 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
4 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
5 | 4 | cv 1541 |
. . . . . . . . 9
class 𝑓 |
6 | 3, 5 | cfv 6339 |
. . . . . . . 8
class (𝑓‘𝑦) |
7 | | cabs 14683 |
. . . . . . . 8
class
abs |
8 | 6, 7 | cfv 6339 |
. . . . . . 7
class
(abs‘(𝑓‘𝑦)) |
9 | | vm |
. . . . . . . 8
setvar 𝑚 |
10 | 9 | cv 1541 |
. . . . . . 7
class 𝑚 |
11 | | cle 10754 |
. . . . . . 7
class
≤ |
12 | 8, 10, 11 | wbr 5030 |
. . . . . 6
wff
(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
13 | 5 | cdm 5525 |
. . . . . . 7
class dom 𝑓 |
14 | | vx |
. . . . . . . . 9
setvar 𝑥 |
15 | 14 | cv 1541 |
. . . . . . . 8
class 𝑥 |
16 | | cpnf 10750 |
. . . . . . . 8
class
+∞ |
17 | | cico 12823 |
. . . . . . . 8
class
[,) |
18 | 15, 16, 17 | co 7170 |
. . . . . . 7
class (𝑥[,)+∞) |
19 | 13, 18 | cin 3842 |
. . . . . 6
class (dom
𝑓 ∩ (𝑥[,)+∞)) |
20 | 12, 2, 19 | wral 3053 |
. . . . 5
wff
∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
21 | | cr 10614 |
. . . . 5
class
ℝ |
22 | 20, 9, 21 | wrex 3054 |
. . . 4
wff
∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
23 | 22, 14, 21 | wrex 3054 |
. . 3
wff
∃𝑥 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚 |
24 | | cc 10613 |
. . . 4
class
ℂ |
25 | | cpm 8438 |
. . . 4
class
↑pm |
26 | 24, 21, 25 | co 7170 |
. . 3
class (ℂ
↑pm ℝ) |
27 | 23, 4, 26 | crab 3057 |
. 2
class {𝑓 ∈ (ℂ
↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚} |
28 | 1, 27 | wceq 1542 |
1
wff
𝑂(1) = {𝑓
∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚} |