# Metamath Proof Explorer

## Theorem supxrgtmnf

Description: The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006)

Ref Expression
Assertion supxrgtmnf ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \mathrm{-\infty }

### Proof

Step Hyp Ref Expression
1 supxrbnd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$
2 1 3expia ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\to sup\left({A},{ℝ}^{*},<\right)\in ℝ\right)$
3 2 con3d ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(¬sup\left({A},{ℝ}^{*},<\right)\in ℝ\to ¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
4 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
5 sstr ${⊢}\left({A}\subseteq ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
6 4 5 mpan2 ${⊢}{A}\subseteq ℝ\to {A}\subseteq {ℝ}^{*}$
7 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
8 6 7 syl ${⊢}{A}\subseteq ℝ\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
9 8 adantr ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
10 nltpnft ${⊢}sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
11 9 10 syl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left({A},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
12 3 11 sylibrd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(¬sup\left({A},{ℝ}^{*},<\right)\in ℝ\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
13 12 orrd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(sup\left({A},{ℝ}^{*},<\right)\in ℝ\vee sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
14 mnfltxr ${⊢}\left(sup\left({A},{ℝ}^{*},<\right)\in ℝ\vee sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \mathrm{-\infty }
15 13 14 syl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \mathrm{-\infty }