# Metamath Proof Explorer

## Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion supxrleub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}\right)$

### Proof

Step Hyp Ref Expression
1 supxrlub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({B}
2 1 notbid ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬{B}
3 ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}<{x}$
4 2 3 syl6bbr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬{B}
5 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
6 xrlenlt ${⊢}\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le {B}↔¬{B}
7 5 6 sylan ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le {B}↔¬{B}
8 simpl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
9 8 sselda ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {x}\in {ℝ}^{*}$
10 simplr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {B}\in {ℝ}^{*}$
11 9 10 xrlenltd ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to \left({x}\le {B}↔¬{B}<{x}\right)$
12 11 ralbidva ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\right)$
13 4 7 12 3bitr4d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}\right)$