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

Metamath Proof Explorer

Theorem suprclrnmpt

Description: Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in maps-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypotheses	suprclrnmpt.x	$⊢ Ⅎ x φ$
		suprclrnmpt.n	$⊢ φ \to A \neq \emptyset$
		suprclrnmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ$
		suprclrnmpt.y	$⊢ φ \to \exists y \in ℝ \forall x \in A B \leq y$
	Assertion	suprclrnmpt	$⊢ φ \to sup (ran (x \in A ⟼ B) ℝ <) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		suprclrnmpt.x	$⊢ Ⅎ x φ$
2		suprclrnmpt.n	$⊢ φ \to A \neq \emptyset$
3		suprclrnmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ$
4		suprclrnmpt.y	$⊢ φ \to \exists y \in ℝ \forall x \in A B \leq y$
5		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
6	1 5 3	rnmptssd	$⊢ φ \to ran (x \in A ⟼ B) \subseteq ℝ$
7	1 3 5 2	rnmptn0	$⊢ φ \to ran (x \in A ⟼ B) \neq \emptyset$
8	1 4	rnmptbdd	$⊢ φ \to \exists y \in ℝ \forall z \in ran (x \in A ⟼ B) z \leq y$
9	6 7 8	suprcld	$⊢ φ \to sup (ran (x \in A ⟼ B) ℝ <) \in ℝ$