# Metamath Proof Explorer

## Theorem supxrbnd

Description: The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrbnd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
2 sstr ${⊢}\left({A}\subseteq ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
3 1 2 mpan2 ${⊢}{A}\subseteq ℝ\to {A}\subseteq {ℝ}^{*}$
4 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
5 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
6 xrltne ${⊢}\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to \mathrm{+\infty }\ne sup\left({A},{ℝ}^{*},<\right)$
7 5 6 mp3an2 ${⊢}\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to \mathrm{+\infty }\ne sup\left({A},{ℝ}^{*},<\right)$
8 7 necomd ${⊢}\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to sup\left({A},{ℝ}^{*},<\right)\ne \mathrm{+\infty }$
9 8 ex ${⊢}sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\to sup\left({A},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
10 4 9 syl ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\to sup\left({A},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
11 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)$
12 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
13 12 adantlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
14 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
15 14 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to {x}\in {ℝ}^{*}$
16 xrlenlt ${⊢}\left({y}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left({y}\le {x}↔¬{x}<{y}\right)$
17 16 con2bid ${⊢}\left({y}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left({x}<{y}↔¬{y}\le {x}\right)$
18 13 15 17 syl2anc ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to \left({x}<{y}↔¬{y}\le {x}\right)$
19 18 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)$
20 rexnal ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}\le {x}↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
21 19 20 syl6bb ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
22 21 ralbidva ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
23 11 22 bitr3d ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
24 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}$
25 23 24 syl6bb ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
26 25 necon2abid ${⊢}{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)\ne \mathrm{+\infty }\right)$
27 10 26 sylibrd ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
28 27 imp ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
29 3 28 sylan ${⊢}\left({A}\subseteq ℝ\wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
30 29 3adant2 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
31 supxrre ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)=sup\left({A},ℝ,<\right)$
32 suprcl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\in ℝ$
33 31 32 eqeltrd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$
34 30 33 syld3an3 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$