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