Detailed syntax breakdown of Definition df-lo1
Step | Hyp | Ref
| Expression |
1 | | clo1 15206 |
. 2
class
≤𝑂(1) |
2 | | vy |
. . . . . . . . 9
setvar 𝑦 |
3 | 2 | cv 1538 |
. . . . . . . 8
class 𝑦 |
4 | | vf |
. . . . . . . . 9
setvar 𝑓 |
5 | 4 | cv 1538 |
. . . . . . . 8
class 𝑓 |
6 | 3, 5 | cfv 6426 |
. . . . . . 7
class (𝑓‘𝑦) |
7 | | vm |
. . . . . . . 8
setvar 𝑚 |
8 | 7 | cv 1538 |
. . . . . . 7
class 𝑚 |
9 | | cle 11020 |
. . . . . . 7
class
≤ |
10 | 6, 8, 9 | wbr 5073 |
. . . . . 6
wff (𝑓‘𝑦) ≤ 𝑚 |
11 | 5 | cdm 5584 |
. . . . . . 7
class dom 𝑓 |
12 | | vx |
. . . . . . . . 9
setvar 𝑥 |
13 | 12 | cv 1538 |
. . . . . . . 8
class 𝑥 |
14 | | cpnf 11016 |
. . . . . . . 8
class
+∞ |
15 | | cico 13091 |
. . . . . . . 8
class
[,) |
16 | 13, 14, 15 | co 7267 |
. . . . . . 7
class (𝑥[,)+∞) |
17 | 11, 16 | cin 3885 |
. . . . . 6
class (dom
𝑓 ∩ (𝑥[,)+∞)) |
18 | 10, 2, 17 | wral 3064 |
. . . . 5
wff
∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚 |
19 | | cr 10880 |
. . . . 5
class
ℝ |
20 | 18, 7, 19 | wrex 3065 |
. . . 4
wff
∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚 |
21 | 20, 12, 19 | wrex 3065 |
. . 3
wff
∃𝑥 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚 |
22 | | cpm 8603 |
. . . 4
class
↑pm |
23 | 19, 19, 22 | co 7267 |
. . 3
class (ℝ
↑pm ℝ) |
24 | 21, 4, 23 | crab 3068 |
. 2
class {𝑓 ∈ (ℝ
↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚} |
25 | 1, 24 | wceq 1539 |
1
wff
≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ)
∣ ∃𝑥 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑦 ∈
(dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚} |