Metamath Proof Explorer

Theorem o1dm

Description: An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion o1dm 
|- ( F e. O(1) -> dom F C_ RR )

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 simprbi 
 |-  ( F e. ( CC ^pm RR ) -> dom F C_ RR )
7 2 6 syl 
 |-  ( F e. O(1) -> dom F C_ RR )