# Metamath Proof Explorer

## Theorem infxrpnf2

Description: Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

### Proof

Step Hyp Ref Expression
1 ssdifss ${⊢}{A}\subseteq {ℝ}^{*}\to {A}\setminus \left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}$
2 infxrpnf ${⊢}{A}\setminus \left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}\to sup\left(\left({A}\setminus \left\{\mathrm{+\infty }\right\}\right)\cup \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)$
3 1 2 syl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left(\left({A}\setminus \left\{\mathrm{+\infty }\right\}\right)\cup \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)$
4 3 adantr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {A}\right)\to sup\left(\left({A}\setminus \left\{\mathrm{+\infty }\right\}\right)\cup \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)$
5 difsnid ${⊢}\mathrm{+\infty }\in {A}\to \left({A}\setminus \left\{\mathrm{+\infty }\right\}\right)\cup \left\{\mathrm{+\infty }\right\}={A}$
6 5 infeq1d ${⊢}\mathrm{+\infty }\in {A}\to sup\left(\left({A}\setminus \left\{\mathrm{+\infty }\right\}\right)\cup \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
7 6 adantl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {A}\right)\to sup\left(\left({A}\setminus \left\{\mathrm{+\infty }\right\}\right)\cup \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
8 4 7 eqtr3d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {A}\right)\to sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
9 difsn ${⊢}¬\mathrm{+\infty }\in {A}\to {A}\setminus \left\{\mathrm{+\infty }\right\}={A}$
10 9 infeq1d ${⊢}¬\mathrm{+\infty }\in {A}\to sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
11 10 adantl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge ¬\mathrm{+\infty }\in {A}\right)\to sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$
12 8 11 pm2.61dan ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A}\setminus \left\{\mathrm{+\infty }\right\},{ℝ}^{*},<\right)=sup\left({A},{ℝ}^{*},<\right)$