Step |
Hyp |
Ref |
Expression |
0 |
|
co1 |
⊢ 𝑂(1) |
1 |
|
vf |
⊢ 𝑓 |
2 |
|
cc |
⊢ ℂ |
3 |
|
cpm |
⊢ ↑pm |
4 |
|
cr |
⊢ ℝ |
5 |
2 4 3
|
co |
⊢ ( ℂ ↑pm ℝ ) |
6 |
|
vx |
⊢ 𝑥 |
7 |
|
vm |
⊢ 𝑚 |
8 |
|
vy |
⊢ 𝑦 |
9 |
1
|
cv |
⊢ 𝑓 |
10 |
9
|
cdm |
⊢ dom 𝑓 |
11 |
6
|
cv |
⊢ 𝑥 |
12 |
|
cico |
⊢ [,) |
13 |
|
cpnf |
⊢ +∞ |
14 |
11 13 12
|
co |
⊢ ( 𝑥 [,) +∞ ) |
15 |
10 14
|
cin |
⊢ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) |
16 |
|
cabs |
⊢ abs |
17 |
8
|
cv |
⊢ 𝑦 |
18 |
17 9
|
cfv |
⊢ ( 𝑓 ‘ 𝑦 ) |
19 |
18 16
|
cfv |
⊢ ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) |
20 |
|
cle |
⊢ ≤ |
21 |
7
|
cv |
⊢ 𝑚 |
22 |
19 21 20
|
wbr |
⊢ ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) ≤ 𝑚 |
23 |
22 8 15
|
wral |
⊢ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) ≤ 𝑚 |
24 |
23 7 4
|
wrex |
⊢ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) ≤ 𝑚 |
25 |
24 6 4
|
wrex |
⊢ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) ≤ 𝑚 |
26 |
25 1 5
|
crab |
⊢ { 𝑓 ∈ ( ℂ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) ≤ 𝑚 } |
27 |
0 26
|
wceq |
⊢ 𝑂(1) = { 𝑓 ∈ ( ℂ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝑓 ‘ 𝑦 ) ) ≤ 𝑚 } |