Metamath Proof Explorer


Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 supxrlub
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( B < sup ( A , RR* , < ) <-> E. x e. A B < x ) )
2 1 notbid
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( -. B < sup ( A , RR* , < ) <-> -. E. x e. A B < x ) )
3 ralnex
 |-  ( A. x e. A -. B < x <-> -. E. x e. A B < x )
4 2 3 bitr4di
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( -. B < sup ( A , RR* , < ) <-> A. x e. A -. B < x ) )
5 supxrcl
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
6 xrlenlt
 |-  ( ( sup ( A , RR* , < ) e. RR* /\ B e. RR* ) -> ( sup ( A , RR* , < ) <_ B <-> -. B < sup ( A , RR* , < ) ) )
7 5 6 sylan
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( sup ( A , RR* , < ) <_ B <-> -. B < sup ( A , RR* , < ) ) )
8 simpl
 |-  ( ( A C_ RR* /\ B e. RR* ) -> A C_ RR* )
9 8 sselda
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> x e. RR* )
10 simplr
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> B e. RR* )
11 9 10 xrlenltd
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> ( x <_ B <-> -. B < x ) )
12 11 ralbidva
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. A x <_ B <-> A. x e. A -. B < x ) )
13 4 7 12 3bitr4d
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( sup ( A , RR* , < ) <_ B <-> A. x e. A x <_ B ) )