Metamath Proof Explorer

Theorem suprleub

Description: The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion suprleub 
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )

Proof

Step Hyp Ref Expression
1 suprnub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( -. B < sup ( A , RR , < ) <-> A. w e. A -. B < w ) )
2 suprcl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
3 lenlt 
 |-  ( ( sup ( A , RR , < ) e. RR /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> -. B < sup ( A , RR , < ) ) )
4 2 3 sylan 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> -. B < sup ( A , RR , < ) ) )
5 simpl1 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> A C_ RR )
6 5 sselda 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) /\ w e. A ) -> w e. RR )
7 simplr 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) /\ w e. A ) -> B e. RR )
8 6 7 lenltd 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) /\ w e. A ) -> ( w <_ B <-> -. B < w ) )
9 8 ralbidva 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( A. w e. A w <_ B <-> A. w e. A -. B < w ) )
10 1 4 9 3bitr4d 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> A. w e. A w <_ B ) )
11 breq1 
 |-  ( w = z -> ( w <_ B <-> z <_ B ) )
12 11 cbvralvw 
 |-  ( A. w e. A w <_ B <-> A. z e. A z <_ B )
13 10 12 bitrdi 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )