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

Metamath Proof Explorer

Theorem suprlub

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

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 1 a1i 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> < Or RR )
3 sup3 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. w e. A y < w ) ) )
4 simp1 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> A C_ RR )
5 2 3 4 suplub2 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( B < sup ( A , RR , < ) <-> E. w e. A B < w ) )
6 breq2 
 |-  ( w = z -> ( B < w <-> B < z ) )
7 6 cbvrexvw 
 |-  ( E. w e. A B < w <-> E. z e. A B < z )
8 5 7 bitrdi 
 |-  ( ( ( 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 ) )