Theorem lo1f

Description: An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Assertion	lo1f	|- ( F e. <_O(1) -> F : dom F --> RR )

Proof

Step	Hyp	Ref	Expression
1		ello1	|- ( F e. <_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 ) )
2	1	simplbi	|- ( F e. <_O(1) -> F e. ( RR ^pm RR ) )
3		reex	|- RR e. _V
4	3 3	elpm2	|- ( F e. ( RR ^pm RR ) <-> ( F : dom F --> RR /\ dom F C_ RR ) )
5	4	simplbi	|- ( F e. ( RR ^pm RR ) -> F : dom F --> RR )
6	2 5	syl	|- ( F e. <_O(1) -> F : dom F --> RR )