Theorem supxrub

Description: A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006)

	Ref	Expression
Assertion	supxrub	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to B\le sup\left(A,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssel2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to B\in {ℝ}^{*}$$
2		supxrcl	$$⊢A\subseteq {ℝ}^{*}\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
3	2	adantr	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
4		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
5	4	a1i	$$⊢A\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$$
6		xrsupss	$$⊢A\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in A\neg x<y\wedge \forall y\in {ℝ}^{*}\left(y<x\to \exists z\in Ay<z\right)\right)$$
7	5 6	supub	$$⊢A\subseteq {ℝ}^{*}\to \left(B\in A\to \neg sup\left(A,{ℝ}^{*},<\right)<B\right)$$
8	7	imp	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to \neg sup\left(A,{ℝ}^{*},<\right)<B$$
9	1 3 8	xrnltled	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to B\le sup\left(A,{ℝ}^{*},<\right)$$