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