Description: A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sup3i.1 | |- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) |
|
Assertion | suprubii | |- ( B e. A -> B <_ sup ( A , RR , < ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sup3i.1 | |- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) |
|
2 | suprub | |- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. A ) -> B <_ sup ( A , RR , < ) ) |
|
3 | 1 2 | mpan | |- ( B e. A -> B <_ sup ( A , RR , < ) ) |