# Metamath Proof Explorer

## Theorem supxr2

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

Ref Expression
Assertion supxr2 ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}\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 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in {A}\right)\to {x}\in {ℝ}^{*}$
2 xrlenlt ${⊢}\left({x}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({x}\le {B}↔¬{B}<{x}\right)$
3 1 2 sylan ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in {A}\right)\wedge {B}\in {ℝ}^{*}\right)\to \left({x}\le {B}↔¬{B}<{x}\right)$
4 3 an32s ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to \left({x}\le {B}↔¬{B}<{x}\right)$
5 4 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)$
6 5 anbi1d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)↔\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)$
7 6 biimpa ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}\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 \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)$
8 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}$
9 7 8 syldan ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {B}\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}$