# Metamath Proof Explorer

## Theorem supxrbnd1

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006)

Ref Expression
Assertion supxrbnd1 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 ralnex ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}$
2 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
3 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
4 xrlenlt ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({x}\le {y}↔¬{y}<{x}\right)$
5 2 3 4 syl2anr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\wedge {x}\in ℝ\right)\to \left({x}\le {y}↔¬{y}<{x}\right)$
6 5 an32s ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to \left({x}\le {y}↔¬{y}<{x}\right)$
7 6 rexbidva ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\right)$
8 rexnal ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}$
9 7 8 syl6rbb ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
10 9 ralbidva ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
11 1 10 bitr3id ${⊢}{A}\subseteq {ℝ}^{*}\to \left(¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
12 supxrunb1 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
13 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
14 nltpnft ${⊢}sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
15 13 14 syl ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
16 11 12 15 3bitrd ${⊢}{A}\subseteq {ℝ}^{*}\to \left(¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
17 16 con4bid ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{x}↔sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$