Metamath Proof Explorer

Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
2 1 a1i ${⊢}{A}\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$
3 xrinfmss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {z}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{z}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({z}<{y}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
4 id ${⊢}{A}\subseteq {ℝ}^{*}\to {A}\subseteq {ℝ}^{*}$
5 2 3 4 infglbb ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)<{B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{B}\right)$
6 5 notbid ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬sup\left({A},{ℝ}^{*},<\right)<{B}↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{B}\right)$
7 ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{B}↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{B}$
8 6 7 syl6bbr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬sup\left({A},{ℝ}^{*},<\right)<{B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{B}\right)$
9 id ${⊢}{B}\in {ℝ}^{*}\to {B}\in {ℝ}^{*}$
10 infxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
11 xrlenlt ${⊢}\left({B}\in {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\to \left({B}\le sup\left({A},{ℝ}^{*},<\right)↔¬sup\left({A},{ℝ}^{*},<\right)<{B}\right)$
12 9 10 11 syl2anr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({B}\le sup\left({A},{ℝ}^{*},<\right)↔¬sup\left({A},{ℝ}^{*},<\right)<{B}\right)$
13 simplr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {B}\in {ℝ}^{*}$
14 simpl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
15 14 sselda ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {x}\in {ℝ}^{*}$
16 13 15 xrlenltd ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to \left({B}\le {x}↔¬{x}<{B}\right)$
17 16 ralbidva ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {x}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{B}\right)$
18 8 12 17 3bitr4d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({B}\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {x}\right)$