This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suprclii

Description: Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999)

		Ref	Expression
	Hypothesis	sup3i.1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
	Assertion	suprclii	$⊢ sup (A ℝ <) \in ℝ$

Step	Hyp	Ref	Expression
1		sup3i.1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
2		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
3	1 2	ax-mp	$⊢ sup (A ℝ <) \in ℝ$