# Metamath Proof Explorer

## Theorem suprcl

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

Ref Expression
Assertion suprcl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 ltso ${⊢}<\mathrm{Or}ℝ$
2 1 a1i ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to <\mathrm{Or}ℝ$
3 sup3 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
4 2 3 supcl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\in ℝ$