# Metamath Proof Explorer

## Theorem infxrlb

Description: A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

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

### Proof

Step Hyp Ref Expression
1 infxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
2 1 adantr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
3 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to {B}\in {ℝ}^{*}$
4 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
5 4 a1i ${⊢}{A}\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$
6 xrinfmss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
7 5 6 inflb ${⊢}{A}\subseteq {ℝ}^{*}\to \left({B}\in {A}\to ¬{B}
8 7 imp ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to ¬{B}
9 2 3 8 xrnltled ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\le {B}$