Description: A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | supxrubd.1 | |- ( ph -> A C_ RR* ) |
|
supxrubd.2 | |- ( ph -> B e. A ) |
||
supxrubd.3 | |- S = sup ( A , RR* , < ) |
||
Assertion | supxrubd | |- ( ph -> B <_ S ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | supxrubd.1 | |- ( ph -> A C_ RR* ) |
|
2 | supxrubd.2 | |- ( ph -> B e. A ) |
|
3 | supxrubd.3 | |- S = sup ( A , RR* , < ) |
|
4 | supxrub | |- ( ( A C_ RR* /\ B e. A ) -> B <_ sup ( A , RR* , < ) ) |
|
5 | 1 2 4 | syl2anc | |- ( ph -> B <_ sup ( A , RR* , < ) ) |
6 | 5 3 | breqtrrdi | |- ( ph -> B <_ S ) |