# Metamath Proof Explorer

## Theorem supxrunb2

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrunb2 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {ℝ}^{*}\to \left({z}\in {A}\to {z}\in {ℝ}^{*}\right)$
2 pnfnlt ${⊢}{z}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{z}$
3 1 2 syl6 ${⊢}{A}\subseteq {ℝ}^{*}\to \left({z}\in {A}\to ¬\mathrm{+\infty }<{z}\right)$
4 3 ralrimiv ${⊢}{A}\subseteq {ℝ}^{*}\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{z}$
5 4 adantr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{z}$
6 breq1 ${⊢}{x}={z}\to \left({x}<{y}↔{z}<{y}\right)$
7 6 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
8 7 rspcva ${⊢}\left({z}\in ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}$
9 8 adantrr ${⊢}\left({z}\in ℝ\wedge \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\wedge {A}\subseteq {ℝ}^{*}\right)\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}$
10 9 ancoms ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\wedge {A}\subseteq {ℝ}^{*}\right)\wedge {z}\in ℝ\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}$
11 10 exp31 ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\to \left({A}\subseteq {ℝ}^{*}\to \left({z}\in ℝ\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
12 11 a1dd ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\to \left({A}\subseteq {ℝ}^{*}\to \left({z}<\mathrm{+\infty }\to \left({z}\in ℝ\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
13 12 com4r ${⊢}{z}\in ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\to \left({A}\subseteq {ℝ}^{*}\to \left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
14 13 com13 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\to \left({z}\in ℝ\to \left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
15 14 imp ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \left({z}\in ℝ\to \left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
16 15 ralrimiv ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
17 5 16 jca ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{z}\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
18 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
19 supxr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{z}\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
20 18 19 mpanl2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{z}\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
21 17 20 syldan ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
22 21 ex ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
23 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
24 23 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {x}\in {ℝ}^{*}$
25 ltpnf ${⊢}{x}\in ℝ\to {x}<\mathrm{+\infty }$
26 breq2 ${⊢}sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left({x}
27 25 26 syl5ibr ${⊢}sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left({x}\in ℝ\to {x}
28 27 impcom ${⊢}\left({x}\in ℝ\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {x}
29 28 adantll ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {x}
30 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
31 30 a1i ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to <\mathrm{Or}{ℝ}^{*}$
32 xrsupss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {z}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}¬{z}<{w}\wedge \forall {w}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{z}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}<{y}\right)\right)$
33 32 ad2antrr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \exists {z}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}¬{z}<{w}\wedge \forall {w}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{z}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}<{y}\right)\right)$
34 31 33 suplub ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \left(\left({x}\in {ℝ}^{*}\wedge {x}
35 24 29 34 mp2and ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}$
36 35 exp31 ${⊢}{A}\subseteq {ℝ}^{*}\to \left({x}\in ℝ\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
37 36 com23 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left({x}\in ℝ\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
38 37 ralrimdv ${⊢}{A}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
39 22 38 impbid ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$