This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 < 𝐵 ↔ 𝑧 < 𝐵 ) )
2 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 < 𝑦 ↔ 𝑧 < 𝑦 ) )
3 2 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
4 1 3 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ↔ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
5 4 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ↔ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
6 elxr ⊢ ( 𝑥 ∈ ℝ* ↔ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) )
7 pm2.27 ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
8 7 a1i ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( 𝑥 ∈ ℝ → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
9 pnfnlt ⊢ ( 𝐵 ∈ ℝ* → ¬ +∞ < 𝐵 )
10 breq1 ⊢ ( 𝑥 = +∞ → ( 𝑥 < 𝐵 ↔ +∞ < 𝐵 ) )
11 10 notbid ⊢ ( 𝑥 = +∞ → ( ¬ 𝑥 < 𝐵 ↔ ¬ +∞ < 𝐵 ) )
12 9 11 imbitrrid ⊢ ( 𝑥 = +∞ → ( 𝐵 ∈ ℝ* → ¬ 𝑥 < 𝐵 ) )
13 pm2.21 ⊢ ( ¬ 𝑥 < 𝐵 → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
14 12 13 syl6com ⊢ ( 𝐵 ∈ ℝ* → ( 𝑥 = +∞ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
15 14 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( 𝑥 = +∞ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
16 15 a1dd ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( 𝑥 = +∞ → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
17 elxr ⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
18 peano2rem ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
19 breq1 ⊢ ( 𝑧 = ( 𝐵 − 1 ) → ( 𝑧 < 𝐵 ↔ ( 𝐵 − 1 ) < 𝐵 ) )
20 breq1 ⊢ ( 𝑧 = ( 𝐵 − 1 ) → ( 𝑧 < 𝑦 ↔ ( 𝐵 − 1 ) < 𝑦 ) )
21 20 rexbidv ⊢ ( 𝑧 = ( 𝐵 − 1 ) → ( ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
22 19 21 imbi12d ⊢ ( 𝑧 = ( 𝐵 − 1 ) → ( ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ↔ ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) ) )
23 22 rspcv ⊢ ( ( 𝐵 − 1 ) ∈ ℝ → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) ) )
24 18 23 syl ⊢ ( 𝐵 ∈ ℝ → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) ) )
25 24 adantl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) ) )
26 ltm1 ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) < 𝐵 )
27 id ⊢ ( ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) → ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
28 26 27 syl5com ⊢ ( 𝐵 ∈ ℝ → ( ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
29 28 adantl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐵 − 1 ) < 𝐵 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
30 18 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐵 − 1 ) ∈ ℝ )
31 mnflt ⊢ ( ( 𝐵 − 1 ) ∈ ℝ → -∞ < ( 𝐵 − 1 ) )
32 30 31 syl ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → -∞ < ( 𝐵 − 1 ) )
33 mnfxr ⊢ -∞ ∈ ℝ*
34 30 rexrd ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐵 − 1 ) ∈ ℝ* )
35 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
36 35 adantlr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
37 xrlttr ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝐵 − 1 ) ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( -∞ < ( 𝐵 − 1 ) ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ < 𝑦 ) )
38 33 34 36 37 mp3an2i ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ( -∞ < ( 𝐵 − 1 ) ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ < 𝑦 ) )
39 32 38 mpand ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐵 − 1 ) < 𝑦 → -∞ < 𝑦 ) )
40 39 reximdva ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
41 25 29 40 3syld ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
42 41 a1dd ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) ) )
43 1re ⊢ 1 ∈ ℝ
44 breq1 ⊢ ( 𝑧 = 1 → ( 𝑧 < 𝐵 ↔ 1 < 𝐵 ) )
45 breq1 ⊢ ( 𝑧 = 1 → ( 𝑧 < 𝑦 ↔ 1 < 𝑦 ) )
46 45 rexbidv ⊢ ( 𝑧 = 1 → ( ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) )
47 44 46 imbi12d ⊢ ( 𝑧 = 1 → ( ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ↔ ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) ) )
48 47 rspcv ⊢ ( 1 ∈ ℝ → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) ) )
49 43 48 ax-mp ⊢ ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) )
50 ltpnf ⊢ ( 1 ∈ ℝ → 1 < +∞ )
51 43 50 ax-mp ⊢ 1 < +∞
52 breq2 ⊢ ( 𝐵 = +∞ → ( 1 < 𝐵 ↔ 1 < +∞ ) )
53 51 52 mpbiri ⊢ ( 𝐵 = +∞ → 1 < 𝐵 )
54 id ⊢ ( ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) → ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) )
55 53 54 syl5com ⊢ ( 𝐵 = +∞ → ( ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) )
56 mnflt ⊢ ( 1 ∈ ℝ → -∞ < 1 )
57 43 56 ax-mp ⊢ -∞ < 1
58 rexr ⊢ ( 1 ∈ ℝ → 1 ∈ ℝ* )
59 43 58 ax-mp ⊢ 1 ∈ ℝ*
60 xrlttr ⊢ ( ( -∞ ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( -∞ < 1 ∧ 1 < 𝑦 ) → -∞ < 𝑦 ) )
61 33 59 60 mp3an12 ⊢ ( 𝑦 ∈ ℝ* → ( ( -∞ < 1 ∧ 1 < 𝑦 ) → -∞ < 𝑦 ) )
62 57 61 mpani ⊢ ( 𝑦 ∈ ℝ* → ( 1 < 𝑦 → -∞ < 𝑦 ) )
63 35 62 syl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → ( 1 < 𝑦 → -∞ < 𝑦 ) )
64 63 reximdva ⊢ ( 𝐴 ⊆ ℝ* → ( ∃ 𝑦 ∈ 𝐴 1 < 𝑦 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
65 55 64 sylan9r ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 = +∞ ) → ( ( 1 < 𝐵 → ∃ 𝑦 ∈ 𝐴 1 < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
66 49 65 syl5 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 = +∞ ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
67 66 a1dd ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 = +∞ ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) ) )
68 xrltnr ⊢ ( -∞ ∈ ℝ* → ¬ -∞ < -∞ )
69 33 68 ax-mp ⊢ ¬ -∞ < -∞
70 breq2 ⊢ ( 𝐵 = -∞ → ( -∞ < 𝐵 ↔ -∞ < -∞ ) )
71 69 70 mtbiri ⊢ ( 𝐵 = -∞ → ¬ -∞ < 𝐵 )
72 71 adantl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 = -∞ ) → ¬ -∞ < 𝐵 )
73 72 pm2.21d ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 = -∞ ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
74 73 a1d ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 = -∞ ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) ) )
75 42 67 74 3jaodan ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) ) )
76 17 75 sylan2b ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) ) )
77 76 imp ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
78 breq1 ⊢ ( 𝑥 = -∞ → ( 𝑥 < 𝐵 ↔ -∞ < 𝐵 ) )
79 breq1 ⊢ ( 𝑥 = -∞ → ( 𝑥 < 𝑦 ↔ -∞ < 𝑦 ) )
80 79 rexbidv ⊢ ( 𝑥 = -∞ → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) )
81 78 80 imbi12d ⊢ ( 𝑥 = -∞ → ( ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ↔ ( -∞ < 𝐵 → ∃ 𝑦 ∈ 𝐴 -∞ < 𝑦 ) ) )
82 77 81 syl5ibrcom ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( 𝑥 = -∞ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
83 82 a1dd ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( 𝑥 = -∞ → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
84 8 16 83 3jaod ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
85 6 84 biimtrid ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( 𝑥 ∈ ℝ* → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
86 85 com23 ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 ∈ ℝ* → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
87 86 ralimdv2 ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
88 87 ex ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑧 ∈ ℝ ( 𝑧 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
89 5 88 biimtrid ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
90 89 pm2.43d ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
91 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
92 91 imim1i ⊢ ( ( 𝑥 ∈ ℝ* → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ( 𝑥 ∈ ℝ → ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
93 92 ralimi2 ⊢ ( ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
94 90 93 impbid1 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )