Metamath Proof Explorer


Theorem supxrubd

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 )

Proof

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 )