This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suprnub

Description: An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 suprlub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) )
2 1 notbid 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( -. B < sup ( A , RR , < ) <-> -. E. z e. A B < z ) )
3 ralnex 
 |-  ( A. z e. A -. B < z <-> -. E. z e. A B < z )
4 2 3 bitr4di 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )