Theorem supxrcl

Description: The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2	1	a1i	$$⊢A\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$$
3		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)$$
4	2 3	supcl	$$⊢A\subseteq {ℝ}^{*}\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$