# Metamath Proof Explorer

## Theorem suprub

Description: A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004)

Ref Expression
Assertion suprub ${⊢}\left(\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)\wedge {B}\in {A}\right)\to {B}\le sup\left({A},ℝ,<\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\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 {A}\subseteq ℝ$
2 1 sselda ${⊢}\left(\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)\wedge {B}\in {A}\right)\to {B}\in ℝ$
3 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 ℝ$
4 3 adantr ${⊢}\left(\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)\wedge {B}\in {A}\right)\to sup\left({A},ℝ,<\right)\in ℝ$
5 ltso ${⊢}<\mathrm{Or}ℝ$
6 5 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}ℝ$
7 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)$
8 6 7 supub ${⊢}\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 \left({B}\in {A}\to ¬sup\left({A},ℝ,<\right)<{B}\right)$
9 8 imp ${⊢}\left(\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)\wedge {B}\in {A}\right)\to ¬sup\left({A},ℝ,<\right)<{B}$
10 2 4 9 nltled ${⊢}\left(\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)\wedge {B}\in {A}\right)\to {B}\le sup\left({A},ℝ,<\right)$