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\phi$$
	suprclrnmpt.n	$$⊢\phi \to A\ne \varnothing$$
	suprclrnmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	suprclrnmpt.y	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
Assertion	suprclrnmpt	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		suprclrnmpt.x	$$⊢Ⅎx\phi$$
2		suprclrnmpt.n	$$⊢\phi \to A\ne \varnothing$$
3		suprclrnmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
4		suprclrnmpt.y	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
5		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
6	1 5 3	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq ℝ$$
7	1 3 5 2	rnmptn0	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing$$
8	1 4	rnmptbdd	$$⊢\phi \to \exists y\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)z\le y$$
9	6 7 8	suprcld	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)\in ℝ$$