# Metamath Proof Explorer

## Theorem supxrpnf

Description: The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005)

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

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {ℝ}^{*}\to \left({y}\in {A}\to {y}\in {ℝ}^{*}\right)$
2 pnfnlt ${⊢}{y}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{y}$
3 1 2 syl6 ${⊢}{A}\subseteq {ℝ}^{*}\to \left({y}\in {A}\to ¬\mathrm{+\infty }<{y}\right)$
4 3 ralrimiv ${⊢}{A}\subseteq {ℝ}^{*}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}$
5 breq2 ${⊢}{z}=\mathrm{+\infty }\to \left({y}<{z}↔{y}<\mathrm{+\infty }\right)$
6 5 rspcev ${⊢}\left(\mathrm{+\infty }\in {A}\wedge {y}<\mathrm{+\infty }\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}$
7 6 ex ${⊢}\mathrm{+\infty }\in {A}\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
8 7 ralrimivw ${⊢}\mathrm{+\infty }\in {A}\to \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
9 4 8 anim12i ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {A}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
10 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
11 supxr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
12 10 11 mpanl2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
13 9 12 syldan ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$