# Metamath Proof Explorer

## Theorem xrsupsslem

Description: Lemma for xrsupss . (Contributed by NM, 25-Oct-2005)

Ref Expression
Assertion xrsupsslem ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 raleq ${⊢}{A}=\varnothing \to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}↔\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\right)$
2 rexeq ${⊢}{A}=\varnothing \to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}↔\exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
3 2 imbi2d ${⊢}{A}=\varnothing \to \left(\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
4 3 ralbidv ${⊢}{A}=\varnothing \to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
5 1 4 anbi12d ${⊢}{A}=\varnothing \to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
6 5 rexbidv ${⊢}{A}=\varnothing \to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
7 sup3 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
8 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
9 8 anim1i ${⊢}\left({x}\in ℝ\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \left({x}\in {ℝ}^{*}\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
10 9 reximi2 ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
11 7 10 syl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
12 elxr ${⊢}{y}\in {ℝ}^{*}↔\left({y}\in ℝ\vee {y}=\mathrm{+\infty }\vee {y}=\mathrm{-\infty }\right)$
13 simpr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge \left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
14 pnfnlt ${⊢}{x}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{x}$
15 14 adantr ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}=\mathrm{+\infty }\right)\to ¬\mathrm{+\infty }<{x}$
16 breq1 ${⊢}{y}=\mathrm{+\infty }\to \left({y}<{x}↔\mathrm{+\infty }<{x}\right)$
17 16 notbid ${⊢}{y}=\mathrm{+\infty }\to \left(¬{y}<{x}↔¬\mathrm{+\infty }<{x}\right)$
18 17 adantl ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}=\mathrm{+\infty }\right)\to \left(¬{y}<{x}↔¬\mathrm{+\infty }<{x}\right)$
19 15 18 mpbird ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}=\mathrm{+\infty }\right)\to ¬{y}<{x}$
20 19 pm2.21d ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}=\mathrm{+\infty }\right)\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
21 20 ex ${⊢}{x}\in {ℝ}^{*}\to \left({y}=\mathrm{+\infty }\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
22 21 ad2antlr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge \left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \left({y}=\mathrm{+\infty }\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
23 ssel ${⊢}{A}\subseteq ℝ\to \left({z}\in {A}\to {z}\in ℝ\right)$
24 mnflt ${⊢}{z}\in ℝ\to \mathrm{-\infty }<{z}$
25 23 24 syl6 ${⊢}{A}\subseteq ℝ\to \left({z}\in {A}\to \mathrm{-\infty }<{z}\right)$
26 25 ancld ${⊢}{A}\subseteq ℝ\to \left({z}\in {A}\to \left({z}\in {A}\wedge \mathrm{-\infty }<{z}\right)\right)$
27 26 eximdv ${⊢}{A}\subseteq ℝ\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in {A}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge \mathrm{-\infty }<{z}\right)\right)$
28 n0 ${⊢}{A}\ne \varnothing ↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
29 df-rex ${⊢}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge \mathrm{-\infty }<{z}\right)$
30 27 28 29 3imtr4g ${⊢}{A}\subseteq ℝ\to \left({A}\ne \varnothing \to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)$
31 30 imp ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}$
32 31 a1d ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(\mathrm{-\infty }<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)$
33 32 ad2antrr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge {y}=\mathrm{-\infty }\right)\to \left(\mathrm{-\infty }<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)$
34 breq1 ${⊢}{y}=\mathrm{-\infty }\to \left({y}<{x}↔\mathrm{-\infty }<{x}\right)$
35 breq1 ${⊢}{y}=\mathrm{-\infty }\to \left({y}<{z}↔\mathrm{-\infty }<{z}\right)$
36 35 rexbidv ${⊢}{y}=\mathrm{-\infty }\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)$
37 34 36 imbi12d ${⊢}{y}=\mathrm{-\infty }\to \left(\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left(\mathrm{-\infty }<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)\right)$
38 37 adantl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge {y}=\mathrm{-\infty }\right)\to \left(\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left(\mathrm{-\infty }<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)\right)$
39 33 38 mpbird ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge {y}=\mathrm{-\infty }\right)\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
40 39 ex ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\to \left({y}=\mathrm{-\infty }\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
41 40 adantr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge \left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \left({y}=\mathrm{-\infty }\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
42 13 22 41 3jaod ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge \left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \left(\left({y}\in ℝ\vee {y}=\mathrm{+\infty }\vee {y}=\mathrm{-\infty }\right)\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
43 12 42 syl5bi ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\wedge \left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \left({y}\in {ℝ}^{*}\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
44 43 ex ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\to \left(\left({y}\in ℝ\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \left({y}\in {ℝ}^{*}\to \left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
45 44 ralimdv2 ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\to \left(\forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\to \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
46 45 anim2d ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge {x}\in {ℝ}^{*}\right)\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
47 46 reximdva ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
48 47 3adant3 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
49 11 48 mpd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
50 49 3expa ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
51 ralnex ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}↔¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
52 rexnal ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}\le {x}↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
53 ssel2 ${⊢}\left({A}\subseteq ℝ\wedge {y}\in {A}\right)\to {y}\in ℝ$
54 letric ${⊢}\left({y}\in ℝ\wedge {x}\in ℝ\right)\to \left({y}\le {x}\vee {x}\le {y}\right)$
55 54 ord ${⊢}\left({y}\in ℝ\wedge {x}\in ℝ\right)\to \left(¬{y}\le {x}\to {x}\le {y}\right)$
56 53 55 sylan ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in {A}\right)\wedge {x}\in ℝ\right)\to \left(¬{y}\le {x}\to {x}\le {y}\right)$
57 56 an32s ${⊢}\left(\left({A}\subseteq ℝ\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to \left(¬{y}\le {x}\to {x}\le {y}\right)$
58 57 reximdva ${⊢}\left({A}\subseteq ℝ\wedge {x}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}\le {x}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
59 52 58 syl5bir ${⊢}\left({A}\subseteq ℝ\wedge {x}\in ℝ\right)\to \left(¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
60 59 ralimdva ${⊢}{A}\subseteq ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
61 60 imp ${⊢}\left({A}\subseteq ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
62 51 61 sylan2br ${⊢}\left({A}\subseteq ℝ\wedge ¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
63 breq2 ${⊢}{y}={z}\to \left({x}\le {y}↔{x}\le {z}\right)$
64 63 cbvrexvw ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}$
65 64 ralbii ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}$
66 62 65 sylib ${⊢}\left({A}\subseteq ℝ\wedge ¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}$
67 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
68 ssel ${⊢}{A}\subseteq ℝ\to \left({y}\in {A}\to {y}\in ℝ\right)$
69 rexr ${⊢}{y}\in ℝ\to {y}\in {ℝ}^{*}$
70 pnfnlt ${⊢}{y}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{y}$
71 69 70 syl ${⊢}{y}\in ℝ\to ¬\mathrm{+\infty }<{y}$
72 68 71 syl6 ${⊢}{A}\subseteq ℝ\to \left({y}\in {A}\to ¬\mathrm{+\infty }<{y}\right)$
73 72 ralrimiv ${⊢}{A}\subseteq ℝ\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}$
74 73 adantr ${⊢}\left({A}\subseteq ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}$
75 peano2re ${⊢}{y}\in ℝ\to {y}+1\in ℝ$
76 breq1 ${⊢}{x}={y}+1\to \left({x}\le {z}↔{y}+1\le {z}\right)$
77 76 rexbidv ${⊢}{x}={y}+1\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}\right)$
78 77 rspcva ${⊢}\left({y}+1\in ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}$
79 78 adantrr ${⊢}\left({y}+1\in ℝ\wedge \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}$
80 79 ancoms ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\wedge {y}+1\in ℝ\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}$
81 75 80 sylan2 ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\wedge {y}\in ℝ\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}$
82 ssel2 ${⊢}\left({A}\subseteq ℝ\wedge {z}\in {A}\right)\to {z}\in ℝ$
83 ltp1 ${⊢}{y}\in ℝ\to {y}<{y}+1$
84 83 adantr ${⊢}\left({y}\in ℝ\wedge {z}\in ℝ\right)\to {y}<{y}+1$
85 75 ancli ${⊢}{y}\in ℝ\to \left({y}\in ℝ\wedge {y}+1\in ℝ\right)$
86 ltletr ${⊢}\left({y}\in ℝ\wedge {y}+1\in ℝ\wedge {z}\in ℝ\right)\to \left(\left({y}<{y}+1\wedge {y}+1\le {z}\right)\to {y}<{z}\right)$
87 86 3expa ${⊢}\left(\left({y}\in ℝ\wedge {y}+1\in ℝ\right)\wedge {z}\in ℝ\right)\to \left(\left({y}<{y}+1\wedge {y}+1\le {z}\right)\to {y}<{z}\right)$
88 85 87 sylan ${⊢}\left({y}\in ℝ\wedge {z}\in ℝ\right)\to \left(\left({y}<{y}+1\wedge {y}+1\le {z}\right)\to {y}<{z}\right)$
89 84 88 mpand ${⊢}\left({y}\in ℝ\wedge {z}\in ℝ\right)\to \left({y}+1\le {z}\to {y}<{z}\right)$
90 89 ancoms ${⊢}\left({z}\in ℝ\wedge {y}\in ℝ\right)\to \left({y}+1\le {z}\to {y}<{z}\right)$
91 82 90 sylan ${⊢}\left(\left({A}\subseteq ℝ\wedge {z}\in {A}\right)\wedge {y}\in ℝ\right)\to \left({y}+1\le {z}\to {y}<{z}\right)$
92 91 an32s ${⊢}\left(\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\wedge {z}\in {A}\right)\to \left({y}+1\le {z}\to {y}<{z}\right)$
93 92 reximdva ${⊢}\left({A}\subseteq ℝ\wedge {y}\in ℝ\right)\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
94 93 adantll ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\wedge {y}\in ℝ\right)\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}+1\le {z}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
95 81 94 mpd ${⊢}\left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\wedge {y}\in ℝ\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}$
96 95 exp31 ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}\in ℝ\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
97 96 a1dd ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}<\mathrm{+\infty }\to \left({y}\in ℝ\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
98 97 com4r ${⊢}{y}\in ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
99 xrltnr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}\to ¬\mathrm{+\infty }<\mathrm{+\infty }$
100 67 99 ax-mp ${⊢}¬\mathrm{+\infty }<\mathrm{+\infty }$
101 breq1 ${⊢}{y}=\mathrm{+\infty }\to \left({y}<\mathrm{+\infty }↔\mathrm{+\infty }<\mathrm{+\infty }\right)$
102 100 101 mtbiri ${⊢}{y}=\mathrm{+\infty }\to ¬{y}<\mathrm{+\infty }$
103 102 pm2.21d ${⊢}{y}=\mathrm{+\infty }\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
104 103 2a1d ${⊢}{y}=\mathrm{+\infty }\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
105 0re ${⊢}0\in ℝ$
106 breq1 ${⊢}{x}=0\to \left({x}\le {z}↔0\le {z}\right)$
107 106 rexbidv ${⊢}{x}=0\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}0\le {z}\right)$
108 107 rspcva ${⊢}\left(0\in ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}0\le {z}$
109 105 108 mpan ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}0\le {z}$
110 82 24 syl ${⊢}\left({A}\subseteq ℝ\wedge {z}\in {A}\right)\to \mathrm{-\infty }<{z}$
111 110 a1d ${⊢}\left({A}\subseteq ℝ\wedge {z}\in {A}\right)\to \left(0\le {z}\to \mathrm{-\infty }<{z}\right)$
112 111 reximdva ${⊢}{A}\subseteq ℝ\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}0\le {z}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}\right)$
113 109 112 mpan9 ${⊢}\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{z}$
114 113 36 syl5ibr ${⊢}{y}=\mathrm{-\infty }\to \left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
115 114 a1dd ${⊢}{y}=\mathrm{-\infty }\to \left(\left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\wedge {A}\subseteq ℝ\right)\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
116 115 expd ${⊢}{y}=\mathrm{-\infty }\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
117 98 104 116 3jaoi ${⊢}\left({y}\in ℝ\vee {y}=\mathrm{+\infty }\vee {y}=\mathrm{-\infty }\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
118 12 117 sylbi ${⊢}{y}\in {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({A}\subseteq ℝ\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
119 118 com13 ${⊢}{A}\subseteq ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\to \left({y}\in {ℝ}^{*}\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
120 119 imp ${⊢}\left({A}\subseteq ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\right)\to \left({y}\in {ℝ}^{*}\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
121 120 ralrimiv ${⊢}\left({A}\subseteq ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\right)\to \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
122 74 121 jca ${⊢}\left({A}\subseteq ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\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)$
123 breq1 ${⊢}{x}=\mathrm{+\infty }\to \left({x}<{y}↔\mathrm{+\infty }<{y}\right)$
124 123 notbid ${⊢}{x}=\mathrm{+\infty }\to \left(¬{x}<{y}↔¬\mathrm{+\infty }<{y}\right)$
125 124 ralbidv ${⊢}{x}=\mathrm{+\infty }\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}\right)$
126 breq2 ${⊢}{x}=\mathrm{+\infty }\to \left({y}<{x}↔{y}<\mathrm{+\infty }\right)$
127 126 imbi1d ${⊢}{x}=\mathrm{+\infty }\to \left(\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
128 127 ralbidv ${⊢}{x}=\mathrm{+\infty }\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
129 125 128 anbi12d ${⊢}{x}=\mathrm{+\infty }\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\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)$
130 129 rspcev ${⊢}\left(\mathrm{+\infty }\in {ℝ}^{*}\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 \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
131 67 122 130 sylancr ${⊢}\left({A}\subseteq ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {z}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
132 66 131 syldan ${⊢}\left({A}\subseteq ℝ\wedge ¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
133 132 adantlr ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\wedge ¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
134 50 133 pm2.61dan ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
135 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
136 ral0 ${⊢}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬\mathrm{-\infty }<{y}$
137 nltmnf ${⊢}{y}\in {ℝ}^{*}\to ¬{y}<\mathrm{-\infty }$
138 137 pm2.21d ${⊢}{y}\in {ℝ}^{*}\to \left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
139 138 rgen ${⊢}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
140 136 139 pm3.2i ${⊢}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬\mathrm{-\infty }<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
141 breq1 ${⊢}{x}=\mathrm{-\infty }\to \left({x}<{y}↔\mathrm{-\infty }<{y}\right)$
142 141 notbid ${⊢}{x}=\mathrm{-\infty }\to \left(¬{x}<{y}↔¬\mathrm{-\infty }<{y}\right)$
143 142 ralbidv ${⊢}{x}=\mathrm{-\infty }\to \left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}↔\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬\mathrm{-\infty }<{y}\right)$
144 breq2 ${⊢}{x}=\mathrm{-\infty }\to \left({y}<{x}↔{y}<\mathrm{-\infty }\right)$
145 144 imbi1d ${⊢}{x}=\mathrm{-\infty }\to \left(\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
146 145 ralbidv ${⊢}{x}=\mathrm{-\infty }\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
147 143 146 anbi12d ${⊢}{x}=\mathrm{-\infty }\to \left(\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬\mathrm{-\infty }<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
148 147 rspcev ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge \left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬\mathrm{-\infty }<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<\mathrm{-\infty }\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
149 135 140 148 mp2an ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
150 149 a1i ${⊢}{A}\subseteq ℝ\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
151 6 134 150 pm2.61ne ${⊢}{A}\subseteq ℝ\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
152 151 adantl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {A}\subseteq ℝ\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
153 ssel ${⊢}{A}\subseteq {ℝ}^{*}\to \left({y}\in {A}\to {y}\in {ℝ}^{*}\right)$
154 153 70 syl6 ${⊢}{A}\subseteq {ℝ}^{*}\to \left({y}\in {A}\to ¬\mathrm{+\infty }<{y}\right)$
155 154 ralrimiv ${⊢}{A}\subseteq {ℝ}^{*}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\mathrm{+\infty }<{y}$
156 breq2 ${⊢}{z}=\mathrm{+\infty }\to \left({y}<{z}↔{y}<\mathrm{+\infty }\right)$
157 156 rspcev ${⊢}\left(\mathrm{+\infty }\in {A}\wedge {y}<\mathrm{+\infty }\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}$
158 157 ex ${⊢}\mathrm{+\infty }\in {A}\to \left({y}<\mathrm{+\infty }\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
159 158 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)$
160 155 159 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)$
161 67 160 130 sylancr ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {A}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
162 152 161 jaodan ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$