Definition df-lo1

Description: Define the set of eventually upper bounded real functions. This fills a gap in O(1) coverage, to express statements like f ( x ) <_ g ( x ) + O ( x ) via ( x e. RR+ |-> ( f ( x ) - g ( x ) ) / x ) e. <_O(1) . (Contributed by Mario Carneiro, 25-May-2016)

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

Detailed syntax breakdown

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