# Metamath Proof Explorer

## Theorem xrinfmsslem

Description: Lemma for xrinfmss . (Contributed by NM, 19-Jan-2006)

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