# Metamath Proof Explorer

## Theorem supxrunb1

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

Ref Expression
Assertion supxrunb1 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {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}\le {y}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{z}$
6 peano2re ${⊢}{z}\in ℝ\to {z}+1\in ℝ$
7 breq1 ${⊢}{x}={z}+1\to \left({x}\le {y}↔{z}+1\le {y}\right)$
8 7 rexbidv ${⊢}{x}={z}+1\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}\right)$
9 8 rspcva ${⊢}\left({z}+1\in ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}$
10 9 adantrr ${⊢}\left({z}+1\in ℝ\wedge \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {A}\subseteq {ℝ}^{*}\right)\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}$
11 10 ancoms ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {A}\subseteq {ℝ}^{*}\right)\wedge {z}+1\in ℝ\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}$
12 6 11 sylan2 ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {A}\subseteq {ℝ}^{*}\right)\wedge {z}\in ℝ\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}$
13 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
14 ltp1 ${⊢}{z}\in ℝ\to {z}<{z}+1$
15 14 adantr ${⊢}\left({z}\in ℝ\wedge {y}\in {ℝ}^{*}\right)\to {z}<{z}+1$
16 6 ancli ${⊢}{z}\in ℝ\to \left({z}\in ℝ\wedge {z}+1\in ℝ\right)$
17 rexr ${⊢}{z}\in ℝ\to {z}\in {ℝ}^{*}$
18 rexr ${⊢}{z}+1\in ℝ\to {z}+1\in {ℝ}^{*}$
19 xrltletr ${⊢}\left({z}\in {ℝ}^{*}\wedge {z}+1\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left(\left({z}<{z}+1\wedge {z}+1\le {y}\right)\to {z}<{y}\right)$
20 18 19 syl3an2 ${⊢}\left({z}\in {ℝ}^{*}\wedge {z}+1\in ℝ\wedge {y}\in {ℝ}^{*}\right)\to \left(\left({z}<{z}+1\wedge {z}+1\le {y}\right)\to {z}<{y}\right)$
21 17 20 syl3an1 ${⊢}\left({z}\in ℝ\wedge {z}+1\in ℝ\wedge {y}\in {ℝ}^{*}\right)\to \left(\left({z}<{z}+1\wedge {z}+1\le {y}\right)\to {z}<{y}\right)$
22 21 3expa ${⊢}\left(\left({z}\in ℝ\wedge {z}+1\in ℝ\right)\wedge {y}\in {ℝ}^{*}\right)\to \left(\left({z}<{z}+1\wedge {z}+1\le {y}\right)\to {z}<{y}\right)$
23 16 22 sylan ${⊢}\left({z}\in ℝ\wedge {y}\in {ℝ}^{*}\right)\to \left(\left({z}<{z}+1\wedge {z}+1\le {y}\right)\to {z}<{y}\right)$
24 15 23 mpand ${⊢}\left({z}\in ℝ\wedge {y}\in {ℝ}^{*}\right)\to \left({z}+1\le {y}\to {z}<{y}\right)$
25 24 ancoms ${⊢}\left({y}\in {ℝ}^{*}\wedge {z}\in ℝ\right)\to \left({z}+1\le {y}\to {z}<{y}\right)$
26 13 25 sylan ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\wedge {z}\in ℝ\right)\to \left({z}+1\le {y}\to {z}<{y}\right)$
27 26 an32s ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {z}\in ℝ\right)\wedge {y}\in {A}\right)\to \left({z}+1\le {y}\to {z}<{y}\right)$
28 27 reximdva ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {z}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
29 28 adantll ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {A}\subseteq {ℝ}^{*}\right)\wedge {z}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}+1\le {y}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
30 12 29 mpd ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {A}\subseteq {ℝ}^{*}\right)\wedge {z}\in ℝ\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}$
31 30 exp31 ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({A}\subseteq {ℝ}^{*}\to \left({z}\in ℝ\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
32 31 a1dd ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {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)$
33 32 com4r ${⊢}{z}\in ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({A}\subseteq {ℝ}^{*}\to \left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
34 33 com13 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({z}\in ℝ\to \left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
35 34 imp ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \left({z}\in ℝ\to \left({z}<\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
36 35 ralrimiv ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {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)$
37 5 36 jca ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {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)$
38 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
39 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 }$
40 38 39 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 }$
41 37 40 syldan ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
42 41 ex ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
43 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
44 43 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {x}\in {ℝ}^{*}$
45 ltpnf ${⊢}{x}\in ℝ\to {x}<\mathrm{+\infty }$
46 breq2 ${⊢}sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left({x}
47 45 46 syl5ibr ${⊢}sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left({x}\in ℝ\to {x}
48 47 impcom ${⊢}\left({x}\in ℝ\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {x}
49 48 adantll ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {x}
50 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
51 50 a1i ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to <\mathrm{Or}{ℝ}^{*}$
52 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)$
53 52 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)$
54 51 53 suplub ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \left(\left({x}\in {ℝ}^{*}\wedge {x}
55 44 49 54 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}$
56 55 ex ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
57 43 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to {x}\in {ℝ}^{*}$
58 13 adantlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
59 xrltle ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({x}<{y}\to {x}\le {y}\right)$
60 57 58 59 syl2anc ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to \left({x}<{y}\to {x}\le {y}\right)$
61 60 reximdva ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
62 56 61 syld ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
63 62 ralrimdva ${⊢}{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}\le {y}\right)$
64 42 63 impbid ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$