# Metamath Proof Explorer

## Theorem supxrmnf

Description: Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrmnf ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A}\cup \left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 uncom ${⊢}{A}\cup \left\{\mathrm{-\infty }\right\}=\left\{\mathrm{-\infty }\right\}\cup {A}$
2 1 supeq1i ${⊢}sup\left({A}\cup \left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=sup\left(\left\{\mathrm{-\infty }\right\}\cup {A},{ℝ}^{*},<\right)$
3 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
4 snssi ${⊢}\mathrm{-\infty }\in {ℝ}^{*}\to \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
5 3 4 mp1i ${⊢}{A}\subseteq {ℝ}^{*}\to \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
6 id ${⊢}{A}\subseteq {ℝ}^{*}\to {A}\subseteq {ℝ}^{*}$
7 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
8 supsn ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\right)\to sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$
9 7 3 8 mp2an ${⊢}sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$
10 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
11 mnfle ${⊢}sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \mathrm{-\infty }\le sup\left({A},{ℝ}^{*},<\right)$
12 10 11 syl ${⊢}{A}\subseteq {ℝ}^{*}\to \mathrm{-\infty }\le sup\left({A},{ℝ}^{*},<\right)$
13 9 12 eqbrtrid ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)$
14 supxrun ${⊢}\left(\left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\wedge {A}\subseteq {ℝ}^{*}\wedge sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)\right)\to sup\left(\left\{\mathrm{-\infty }\right\}\cup {A},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
15 5 6 13 14 syl3anc ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left(\left\{\mathrm{-\infty }\right\}\cup {A},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
16 2 15 syl5eq ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A}\cup \left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$