# Metamath Proof Explorer

## Theorem suprnub

Description: An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion suprnub ${⊢}\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 ℝ\right)\to \left(¬{B}

### Proof

Step Hyp Ref Expression
1 suprlub ${⊢}\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 ℝ\right)\to \left({B}
2 1 notbid ${⊢}\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 ℝ\right)\to \left(¬{B}
3 ralnex ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{z}↔¬\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{B}<{z}$
4 2 3 syl6bbr ${⊢}\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 ℝ\right)\to \left(¬{B}