# Metamath Proof Explorer

## Theorem supxr

Description: The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006) (Revised by Mario Carneiro, 21-Apr-2015)

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

### Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)\to {B}\in {ℝ}^{*}$
2 simprl ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}$
3 xrub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
4 3 biimpa ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
5 4 adantrl ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
6 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
7 6 a1i ${⊢}\top \to <\mathrm{Or}{ℝ}^{*}$
8 7 eqsup ${⊢}\top \to \left(\left({B}\in {ℝ}^{*}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\wedge \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to sup\left({A},{ℝ}^{*},<\right)={B}\right)$
9 8 mptru ${⊢}\left({B}\in {ℝ}^{*}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\wedge \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to sup\left({A},{ℝ}^{*},<\right)={B}$
10 1 2 5 9 syl3anc ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{x}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)\to sup\left({A},{ℝ}^{*},<\right)={B}$