Definition df-lo1 14222

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.)

Assertion

Ref	Expression
df-lo1	|- <_O(1) = { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m }

Distinct variable group:   x, y, f, m

Detailed syntax breakdown of Definition df-lo1

Step	Hyp	Ref	Expression
1		clo1 14218	. 2 class <_O(1)
2		vy	. . . . . . . . 9 setvar y
3	2	cv 1482	. . . . . . . 8 class y
4		vf	. . . . . . . . 9 setvar f
5	4	cv 1482	. . . . . . . 8 class f
6	3, 5	cfv 5888	. . . . . . 7 class ( f ` y )
7		vm	. . . . . . . 8 setvar m
8	7	cv 1482	. . . . . . 7 class m
9		cle 10075	. . . . . . 7 class <_
10	6, 8, 9	wbr 4653	. . . . . 6 wff ( f ` y ) <_ m
11	5	cdm 5114	. . . . . . 7 class dom f
12		vx	. . . . . . . . 9 setvar x
13	12	cv 1482	. . . . . . . 8 class x
14		cpnf 10071	. . . . . . . 8 class +oo
15		cico 12177	. . . . . . . 8 class [,)
16	13, 14, 15	co 6650	. . . . . . 7 class ( x [,) +oo )
17	11, 16	cin 3573	. . . . . 6 class ( dom f i^i ( x [,) +oo ) )
18	10, 2, 17	wral 2912	. . . . 5 wff A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m
19		cr 9935	. . . . 5 class RR
20	18, 7, 19	wrex 2913	. . . 4 wff E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m
21	20, 12, 19	wrex 2913	. . 3 wff E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m
22		cpm 7858	. . . 4 class ^pm
23	19, 19, 22	co 6650	. . 3 class ( RR ^pm RR )
24	21, 4, 23	crab 2916	. 2 class { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m }
25	1, 24	wceq 1483	1 wff <_O(1) = { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m }

This definition is referenced by:  ello1  14246