Definition df-lo1 15128

Description: Define the set of eventually upper bounded real functions. This fills a gap in 𝑂(1) coverage, to express statements like 𝑓(𝑥) ≤ 𝑔(𝑥) + 𝑂(𝑥) via (𝑥 ∈ ℝ⁺ ↦ (𝑓(𝑥) − 𝑔(𝑥)) / 𝑥) ∈ ≤𝑂(1). (Contributed by Mario Carneiro, 25-May-2016.)

Assertion

Ref	Expression
df-lo1	⊢ ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}

Distinct variable group:   𝑥,𝑦,𝑓,𝑚

Detailed syntax breakdown of Definition df-lo1

Step	Hyp	Ref	Expression
1		clo1 15124	. 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 6418	. . . . . . 7 class (𝑓‘𝑦)
7		vm	. . . . . . . 8 setvar 𝑚
8	7	cv 1538	. . . . . . 7 class 𝑚
9		cle 10941	. . . . . . 7 class ≤
10	6, 8, 9	wbr 5070	. . . . . 6 wff (𝑓‘𝑦) ≤ 𝑚
11	5	cdm 5580	. . . . . . 7 class dom 𝑓
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1538	. . . . . . . 8 class 𝑥
14		cpnf 10937	. . . . . . . 8 class +∞
15		cico 13010	. . . . . . . 8 class [,)
16	13, 14, 15	co 7255	. . . . . . 7 class (𝑥[,)+∞)
17	11, 16	cin 3882	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
18	10, 2, 17	wral 3063	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
19		cr 10801	. . . . 5 class ℝ
20	18, 7, 19	wrex 3064	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
21	20, 12, 19	wrex 3064	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
22		cpm 8574	. . . 4 class ↑pm
23	19, 19, 22	co 7255	. . 3 class (ℝ ↑pm ℝ)
24	21, 4, 23	crab 3067	. 2 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}
25	1, 24	wceq 1539	1 wff ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}

This definition is referenced by:  ello1  15152