# Metamath Proof Explorer

## Theorem supxrub

Description: A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006)

Ref Expression
Assertion supxrub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to {B}\le sup\left({A},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to {B}\in {ℝ}^{*}$
2 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
3 2 adantr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
4 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
5 4 a1i ${⊢}{A}\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$
6 xrsupss ${⊢}{A}\subseteq {ℝ}^{*}\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)$
7 5 6 supub ${⊢}{A}\subseteq {ℝ}^{*}\to \left({B}\in {A}\to ¬sup\left({A},{ℝ}^{*},<\right)<{B}\right)$
8 7 imp ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to ¬sup\left({A},{ℝ}^{*},<\right)<{B}$
9 1 3 8 xrnltled ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to {B}\le sup\left({A},{ℝ}^{*},<\right)$