Metamath Proof Explorer

Theorem supxrlub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Assertion supxrlub 
|- ( ( A C_ RR* /\ B e. RR* ) -> ( B < sup ( A , RR* , < ) <-> E. x e. A B < x ) )

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 1 a1i 
 |-  ( A C_ RR* -> < Or RR* )
3 xrsupss 
 |-  ( A C_ RR* -> E. y e. RR* ( A. z e. A -. y < z /\ A. z e. RR* ( z < y -> E. x e. A z < x ) ) )
4 id 
 |-  ( A C_ RR* -> A C_ RR* )
5 2 3 4 suplub2 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( B < sup ( A , RR* , < ) <-> E. x e. A B < x ) )