Metamath Proof Explorer

Theorem supxrre2

Description: The supremum of a nonempty set of reals is real iff it is not plus infinity. (Contributed by NM, 5-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 supxrre1 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(sup\left({A},{ℝ}^{*},<\right)\in ℝ↔sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
2 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
3 sstr ${⊢}\left({A}\subseteq ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
4 2 3 mpan2 ${⊢}{A}\subseteq ℝ\to {A}\subseteq {ℝ}^{*}$
5 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
6 nltpnft ${⊢}sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
7 4 5 6 3syl ${⊢}{A}\subseteq ℝ\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
8 7 necon2abid ${⊢}{A}\subseteq ℝ\to \left(sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }↔sup\left({A},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
9 8 adantr ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }↔sup\left({A},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
10 1 9 bitrd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(sup\left({A},{ℝ}^{*},<\right)\in ℝ↔sup\left({A},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$