Description: The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Oct-2004) (Revised by Mario Carneiro, 6-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sup3i.1 | |- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) |
|
Assertion | suprlubii | |- ( B e. RR -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sup3i.1 | |- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) |
|
2 | 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 ) ) |
|
3 | 1 2 | mpan | |- ( B e. RR -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) ) |