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 )