Definition df-lo1 15527

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 15523	. 2 class ≤𝑂(1)
2		vy	. . . . . . . . 9 setvar 𝑦
3	2	cv 1539	. . . . . . . 8 class 𝑦
4		vf	. . . . . . . . 9 setvar 𝑓
5	4	cv 1539	. . . . . . . 8 class 𝑓
6	3, 5	cfv 6561	. . . . . . 7 class (𝑓‘𝑦)
7		vm	. . . . . . . 8 setvar 𝑚
8	7	cv 1539	. . . . . . 7 class 𝑚
9		cle 11296	. . . . . . 7 class ≤
10	6, 8, 9	wbr 5143	. . . . . 6 wff (𝑓‘𝑦) ≤ 𝑚
11	5	cdm 5685	. . . . . . 7 class dom 𝑓
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1539	. . . . . . . 8 class 𝑥
14		cpnf 11292	. . . . . . . 8 class +∞
15		cico 13389	. . . . . . . 8 class [,)
16	13, 14, 15	co 7431	. . . . . . 7 class (𝑥[,)+∞)
17	11, 16	cin 3950	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
18	10, 2, 17	wral 3061	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
19		cr 11154	. . . . 5 class ℝ
20	18, 7, 19	wrex 3070	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
21	20, 12, 19	wrex 3070	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚
22		cpm 8867	. . . 4 class ↑pm
23	19, 19, 22	co 7431	. . 3 class (ℝ ↑pm ℝ)
24	21, 4, 23	crab 3436	. 2 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}
25	1, 24	wceq 1540	1 wff ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}

This definition is referenced by:  ello1  15551