Theorem o1f

Description: An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	o1f	|- ( F e. O(1) -> F : dom F --> CC )

Proof

Step	Hyp	Ref	Expression
1		elo1	|- ( F e. O(1) <-> ( F e. ( CC ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )
2	1	simplbi	|- ( F e. O(1) -> F e. ( CC ^pm RR ) )
3		cnex	|- CC e. _V
4		reex	|- RR e. _V
5	3 4	elpm2	|- ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
6	5	simplbi	|- ( F e. ( CC ^pm RR ) -> F : dom F --> CC )
7	2 6	syl	|- ( F e. O(1) -> F : dom F --> CC )