Metamath Proof Explorer

Theorem lo1bdd

Description: The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016)

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

Proof

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