# Metamath Proof Explorer

## Theorem supxrbnd2

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

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