Metamath Proof Explorer


Theorem lo1dm

Description: An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1dm
|- ( F e. <_O(1) -> dom F C_ 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 simprbi
 |-  ( F e. ( RR ^pm RR ) -> dom F C_ RR )
6 2 5 syl
 |-  ( F e. <_O(1) -> dom F C_ RR )