Definition df-lo1 14070

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 14066	. 2 class ≤𝑂(1)
2		vy	. . . . . . . . 9 setvar 𝑦
3	2	cv 1474	. . . . . . . 8 class 𝑦
4		vf	. . . . . . . . 9 setvar 𝑓
5	4	cv 1474	. . . . . . . 8 class 𝑓
6	3, 5	cfv 5804	. . . . . . 7 class (𝑓‘𝑦)
7		vm	. . . . . . . 8 setvar 𝑚
8	7	cv 1474	. . . . . . 7 class 𝑚
9		cle 9954	. . . . . . 7 class ≤
10	6, 8, 9	wbr 4583	. . . . . 6 wff (𝑓‘𝑦) ≤ 𝑚
11	5	cdm 5038	. . . . . . 7 class dom 𝑓
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1474	. . . . . . . 8 class 𝑥
14		cpnf 9950	. . . . . . . 8 class +∞
15		cico 12048	. . . . . . . 8 class [,)
16	13, 14, 15	co 6549	. . . . . . 7 class (𝑥[,)+∞)
17	11, 16	cin 3539	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
18	10, 2, 17	wral 2896	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
19		cr 9814	. . . . 5 class ℝ
20	18, 7, 19	wrex 2897	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
21	20, 12, 19	wrex 2897	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
22		cpm 7745	. . . 4 class ↑pm
23	19, 19, 22	co 6549	. . 3 class (ℝ ↑pm ℝ)
24	21, 4, 23	crab 2900	. 2 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}
25	1, 24	wceq 1475	1 wff ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}

This definition is referenced by:  ello1  14094