Metamath Proof Explorer

Theorem o1bdd

Description: The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion o1bdd 
|- ( ( F e. O(1) /\ F : A --> CC ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> F e. O(1) )
2 simpr 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> F : A --> CC )
3 fdm 
 |-  ( F : A --> CC -> dom F = A )
4 3 adantl 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> dom F = A )
5 o1dm 
 |-  ( F e. O(1) -> dom F C_ RR )
6 5 adantr 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> dom F C_ RR )
7 4 6 eqsstrrd 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> A C_ RR )
8 elo12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
9 2 7 8 syl2anc 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
10 1 9 mpbid 
 |-  ( ( F e. O(1) /\ F : A --> CC ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) )