Theorem supxrcli

Description: The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	supxrcli.1	$$⊢A\subseteq {ℝ}^{*}$$
Assertion	supxrcli	$$⊢sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		supxrcli.1	$$⊢A\subseteq {ℝ}^{*}$$
2		supxrcl	$$⊢A\subseteq {ℝ}^{*}\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
3	1 2	ax-mp	$$⊢sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$