# Metamath Proof Explorer

## Theorem xrub

Description: By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion xrub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{x}={z}\to \left({x}<{B}↔{z}<{B}\right)$
2 breq1 ${⊢}{x}={z}\to \left({x}<{y}↔{z}<{y}\right)$
3 2 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
4 1 3 imbi12d ${⊢}{x}={z}\to \left(\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)↔\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
5 4 cbvralvw ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)↔\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
6 elxr ${⊢}{x}\in {ℝ}^{*}↔\left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)$
7 pm2.27 ${⊢}{x}\in ℝ\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
8 7 a1i ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left({x}\in ℝ\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
9 pnfnlt ${⊢}{B}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{B}$
10 breq1 ${⊢}{x}=\mathrm{+\infty }\to \left({x}<{B}↔\mathrm{+\infty }<{B}\right)$
11 10 notbid ${⊢}{x}=\mathrm{+\infty }\to \left(¬{x}<{B}↔¬\mathrm{+\infty }<{B}\right)$
12 9 11 syl5ibr ${⊢}{x}=\mathrm{+\infty }\to \left({B}\in {ℝ}^{*}\to ¬{x}<{B}\right)$
13 pm2.21 ${⊢}¬{x}<{B}\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
14 12 13 syl6com ${⊢}{B}\in {ℝ}^{*}\to \left({x}=\mathrm{+\infty }\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
15 14 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left({x}=\mathrm{+\infty }\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
16 15 a1dd ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left({x}=\mathrm{+\infty }\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
17 elxr ${⊢}{B}\in {ℝ}^{*}↔\left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)$
18 peano2rem ${⊢}{B}\in ℝ\to {B}-1\in ℝ$
19 breq1 ${⊢}{z}={B}-1\to \left({z}<{B}↔{B}-1<{B}\right)$
20 breq1 ${⊢}{z}={B}-1\to \left({z}<{y}↔{B}-1<{y}\right)$
21 20 rexbidv ${⊢}{z}={B}-1\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)$
22 19 21 imbi12d ${⊢}{z}={B}-1\to \left(\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)↔\left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\right)$
23 22 rspcv ${⊢}{B}-1\in ℝ\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\right)$
24 18 23 syl ${⊢}{B}\in ℝ\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\right)$
25 24 adantl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\right)$
26 ltm1 ${⊢}{B}\in ℝ\to {B}-1<{B}$
27 id ${⊢}\left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\to \left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)$
28 26 27 syl5com ${⊢}{B}\in ℝ\to \left(\left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)$
29 28 adantl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\left({B}-1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\right)$
30 18 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge {y}\in {A}\right)\to {B}-1\in ℝ$
31 mnflt ${⊢}{B}-1\in ℝ\to \mathrm{-\infty }<{B}-1$
32 30 31 syl ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge {y}\in {A}\right)\to \mathrm{-\infty }<{B}-1$
33 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
34 30 rexrd ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge {y}\in {A}\right)\to {B}-1\in {ℝ}^{*}$
35 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
36 35 adantlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge {y}\in {A}\right)\to {y}\in {ℝ}^{*}$
37 xrlttr ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {B}-1\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left(\left(\mathrm{-\infty }<{B}-1\wedge {B}-1<{y}\right)\to \mathrm{-\infty }<{y}\right)$
38 33 34 36 37 mp3an2i ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge {y}\in {A}\right)\to \left(\left(\mathrm{-\infty }<{B}-1\wedge {B}-1<{y}\right)\to \mathrm{-\infty }<{y}\right)$
39 32 38 mpand ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge {y}\in {A}\right)\to \left({B}-1<{y}\to \mathrm{-\infty }<{y}\right)$
40 39 reximdva ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}-1<{y}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
41 25 29 40 3syld ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
42 41 a1dd ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)\right)$
43 1re ${⊢}1\in ℝ$
44 breq1 ${⊢}{z}=1\to \left({z}<{B}↔1<{B}\right)$
45 breq1 ${⊢}{z}=1\to \left({z}<{y}↔1<{y}\right)$
46 45 rexbidv ${⊢}{z}=1\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)$
47 44 46 imbi12d ${⊢}{z}=1\to \left(\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)↔\left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)\right)$
48 47 rspcv ${⊢}1\in ℝ\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)\right)$
49 43 48 ax-mp ${⊢}\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)$
50 ltpnf ${⊢}1\in ℝ\to 1<\mathrm{+\infty }$
51 43 50 ax-mp ${⊢}1<\mathrm{+\infty }$
52 breq2 ${⊢}{B}=\mathrm{+\infty }\to \left(1<{B}↔1<\mathrm{+\infty }\right)$
53 51 52 mpbiri ${⊢}{B}=\mathrm{+\infty }\to 1<{B}$
54 id ${⊢}\left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)\to \left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)$
55 53 54 syl5com ${⊢}{B}=\mathrm{+\infty }\to \left(\left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)$
56 mnflt ${⊢}1\in ℝ\to \mathrm{-\infty }<1$
57 43 56 ax-mp ${⊢}\mathrm{-\infty }<1$
58 rexr ${⊢}1\in ℝ\to 1\in {ℝ}^{*}$
59 43 58 ax-mp ${⊢}1\in {ℝ}^{*}$
60 xrlttr ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left(\left(\mathrm{-\infty }<1\wedge 1<{y}\right)\to \mathrm{-\infty }<{y}\right)$
61 33 59 60 mp3an12 ${⊢}{y}\in {ℝ}^{*}\to \left(\left(\mathrm{-\infty }<1\wedge 1<{y}\right)\to \mathrm{-\infty }<{y}\right)$
62 57 61 mpani ${⊢}{y}\in {ℝ}^{*}\to \left(1<{y}\to \mathrm{-\infty }<{y}\right)$
63 35 62 syl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {y}\in {A}\right)\to \left(1<{y}\to \mathrm{-\infty }<{y}\right)$
64 63 reximdva ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
65 55 64 sylan9r ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}=\mathrm{+\infty }\right)\to \left(\left(1<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}1<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
66 49 65 syl5 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}=\mathrm{+\infty }\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
67 66 a1dd ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}=\mathrm{+\infty }\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)\right)$
68 xrltnr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}\to ¬\mathrm{-\infty }<\mathrm{-\infty }$
69 33 68 ax-mp ${⊢}¬\mathrm{-\infty }<\mathrm{-\infty }$
70 breq2 ${⊢}{B}=\mathrm{-\infty }\to \left(\mathrm{-\infty }<{B}↔\mathrm{-\infty }<\mathrm{-\infty }\right)$
71 69 70 mtbiri ${⊢}{B}=\mathrm{-\infty }\to ¬\mathrm{-\infty }<{B}$
72 71 adantl ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to ¬\mathrm{-\infty }<{B}$
73 72 pm2.21d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
74 73 a1d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)\right)$
75 42 67 74 3jaodan ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)\right)$
76 17 75 sylan2b ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)\right)$
77 76 imp ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
78 breq1 ${⊢}{x}=\mathrm{-\infty }\to \left({x}<{B}↔\mathrm{-\infty }<{B}\right)$
79 breq1 ${⊢}{x}=\mathrm{-\infty }\to \left({x}<{y}↔\mathrm{-\infty }<{y}\right)$
80 79 rexbidv ${⊢}{x}=\mathrm{-\infty }\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)$
81 78 80 imbi12d ${⊢}{x}=\mathrm{-\infty }\to \left(\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)↔\left(\mathrm{-\infty }<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }<{y}\right)\right)$
82 77 81 syl5ibrcom ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left({x}=\mathrm{-\infty }\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
83 82 a1dd ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left({x}=\mathrm{-\infty }\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
84 8 16 83 3jaod ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left(\left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
85 6 84 syl5bi ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left({x}\in {ℝ}^{*}\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
86 85 com23 ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left(\left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}\in {ℝ}^{*}\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
87 86 ralimdv2 ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
88 87 ex ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
89 5 88 syl5bi ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
90 89 pm2.43d ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
91 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
92 91 imim1i ${⊢}\left({x}\in {ℝ}^{*}\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\to \left({x}\in ℝ\to \left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
93 92 ralimi2 ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
94 90 93 impbid1 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$