# Metamath Proof Explorer

## Theorem xrge0infss

Description: Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion xrge0infss ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ssel2 ${⊢}\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {y}\in {A}\right)\to {y}\in \left[0,\mathrm{+\infty }\right]$
2 0xr ${⊢}0\in {ℝ}^{*}$
3 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
4 iccgelb ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le {y}$
5 2 3 4 mp3an12 ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to 0\le {y}$
6 eliccxr ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to {y}\in {ℝ}^{*}$
7 xrlenlt ${⊢}\left(0\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left(0\le {y}↔¬{y}<0\right)$
8 2 6 7 sylancr ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to \left(0\le {y}↔¬{y}<0\right)$
9 5 8 mpbid ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to ¬{y}<0$
10 1 9 syl ${⊢}\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {y}\in {A}\right)\to ¬{y}<0$
11 10 ralrimiva ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<0$
12 11 ad3antrrr ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge {w}\le 0\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<0$
13 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
14 ssralv ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
15 13 14 ax-mp ${⊢}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
16 simplll ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to {w}\in {ℝ}^{*}$
17 2 a1i ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to 0\in {ℝ}^{*}$
18 simplr ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to {y}\in \left[0,\mathrm{+\infty }\right]$
19 13 18 sseldi ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to {y}\in {ℝ}^{*}$
20 simpllr ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to {w}\le 0$
21 simpr ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to 0<{y}$
22 16 17 19 20 21 xrlelttrd ${⊢}\left(\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge 0<{y}\right)\to {w}<{y}$
23 22 ex ${⊢}\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(0<{y}\to {w}<{y}\right)$
24 23 imim1d ${⊢}\left(\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
25 24 ralimdva ${⊢}\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\to \left(\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
26 15 25 syl5 ${⊢}\left({w}\in {ℝ}^{*}\wedge {w}\le 0\right)\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
27 26 adantll ${⊢}\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge {w}\le 0\right)\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
28 27 imp ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge {w}\le 0\right)\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
29 28 adantrl ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge {w}\le 0\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
30 29 an32s ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge {w}\le 0\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
31 0e0iccpnf ${⊢}0\in \left[0,\mathrm{+\infty }\right]$
32 breq2 ${⊢}{x}=0\to \left({y}<{x}↔{y}<0\right)$
33 32 notbid ${⊢}{x}=0\to \left(¬{y}<{x}↔¬{y}<0\right)$
34 33 ralbidv ${⊢}{x}=0\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<0\right)$
35 breq1 ${⊢}{x}=0\to \left({x}<{y}↔0<{y}\right)$
36 35 imbi1d ${⊢}{x}=0\to \left(\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)↔\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
37 36 ralbidv ${⊢}{x}=0\to \left(\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)↔\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
38 34 37 anbi12d ${⊢}{x}=0\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<0\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
39 38 rspcev ${⊢}\left(0\in \left[0,\mathrm{+\infty }\right]\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<0\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
40 31 39 mpan ${⊢}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<0\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(0<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
41 12 30 40 syl2anc ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge {w}\le 0\right)\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
42 simpllr ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge 0\le {w}\right)\to {w}\in {ℝ}^{*}$
43 simpr ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge 0\le {w}\right)\to 0\le {w}$
44 elxrge0 ${⊢}{w}\in \left[0,\mathrm{+\infty }\right]↔\left({w}\in {ℝ}^{*}\wedge 0\le {w}\right)$
45 42 43 44 sylanbrc ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge 0\le {w}\right)\to {w}\in \left[0,\mathrm{+\infty }\right]$
46 15 a1i ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
47 46 anim2d ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
48 47 adantr ${⊢}\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
49 48 imp ${⊢}\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
50 49 adantr ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge 0\le {w}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
51 breq2 ${⊢}{x}={w}\to \left({y}<{x}↔{y}<{w}\right)$
52 51 notbid ${⊢}{x}={w}\to \left(¬{y}<{x}↔¬{y}<{w}\right)$
53 52 ralbidv ${⊢}{x}={w}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\right)$
54 breq1 ${⊢}{x}={w}\to \left({x}<{y}↔{w}<{y}\right)$
55 54 imbi1d ${⊢}{x}={w}\to \left(\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)↔\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
56 55 ralbidv ${⊢}{x}={w}\to \left(\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)↔\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
57 53 56 anbi12d ${⊢}{x}={w}\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
58 57 rspcev ${⊢}\left({w}\in \left[0,\mathrm{+\infty }\right]\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
59 45 50 58 syl2anc ${⊢}\left(\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\wedge 0\le {w}\right)\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
60 simplr ${⊢}\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to {w}\in {ℝ}^{*}$
61 2 a1i ${⊢}\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to 0\in {ℝ}^{*}$
62 xrletri ${⊢}\left({w}\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left({w}\le 0\vee 0\le {w}\right)$
63 60 61 62 syl2anc ${⊢}\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to \left({w}\le 0\vee 0\le {w}\right)$
64 41 59 63 mpjaodan ${⊢}\left(\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge {w}\in {ℝ}^{*}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
65 sstr ${⊢}\left({A}\subseteq \left[0,\mathrm{+\infty }\right]\wedge \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
66 13 65 mpan2 ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to {A}\subseteq {ℝ}^{*}$
67 xrinfmss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {w}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
68 66 67 syl ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to \exists {w}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{w}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({w}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
69 64 68 r19.29a ${⊢}{A}\subseteq \left[0,\mathrm{+\infty }\right]\to \exists {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$