Theorem supxrlub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Assertion	supxrlub	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B<sup\left(A,{ℝ}^{*},<\right)\leftrightarrow \exists x\in AB<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2	1	a1i	$$⊢A\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$$
3		xrsupss	$$⊢A\subseteq {ℝ}^{*}\to \exists y\in {ℝ}^{*}\left(\forall z\in A\neg y<z\wedge \forall z\in {ℝ}^{*}\left(z<y\to \exists x\in Az<x\right)\right)$$
4		id	$$⊢A\subseteq {ℝ}^{*}\to A\subseteq {ℝ}^{*}$$
5	2 3 4	suplub2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B<sup\left(A,{ℝ}^{*},<\right)\leftrightarrow \exists x\in AB<x\right)$$