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	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
	supxrubd.2	$$⊢\phi \to B\in A$$
	supxrubd.3	$$⊢S=sup\left(A,{ℝ}^{*},<\right)$$
Assertion	supxrubd	$$⊢\phi \to B\le S$$

Proof

Step	Hyp	Ref	Expression
1		supxrubd.1	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
2		supxrubd.2	$$⊢\phi \to B\in A$$
3		supxrubd.3	$$⊢S=sup\left(A,{ℝ}^{*},<\right)$$
4		supxrub	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to B\le sup\left(A,{ℝ}^{*},<\right)$$
5	1 2 4	syl2anc	$$⊢\phi \to B\le sup\left(A,{ℝ}^{*},<\right)$$
6	5 3	breqtrrdi	$$⊢\phi \to B\le S$$