Step | Hyp | Ref
| Expression |
1 | | breq1 4656 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 < 𝐵 ↔ 𝑧 < 𝐵)) |
2 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 < 𝑦 ↔ 𝑧 < 𝑦)) |
3 | 2 | rexbidv 3052 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) |
4 | 1, 3 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) ↔ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦))) |
5 | 4 | cbvralv 3171 |
. . . 4
⊢
(∀𝑥 ∈
ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) ↔ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) |
6 | | elxr 11950 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ*
↔ (𝑥 ∈ ℝ
∨ 𝑥 = +∞ ∨
𝑥 =
-∞)) |
7 | | pm2.27 42 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
9 | | pnfnlt 11962 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ*
→ ¬ +∞ < 𝐵) |
10 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = +∞ → (𝑥 < 𝐵 ↔ +∞ < 𝐵)) |
11 | 10 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑥 = +∞ → (¬ 𝑥 < 𝐵 ↔ ¬ +∞ < 𝐵)) |
12 | 9, 11 | syl5ibr 236 |
. . . . . . . . . . . 12
⊢ (𝑥 = +∞ → (𝐵 ∈ ℝ*
→ ¬ 𝑥 < 𝐵)) |
13 | | pm2.21 120 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 < 𝐵 → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) |
14 | 12, 13 | syl6com 37 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝑥 = +∞ →
(𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
15 | 14 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (𝑥 = +∞ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
16 | 15 | a1dd 50 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (𝑥 = +∞ → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
17 | | elxr 11950 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
18 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) |
19 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝐵 − 1) → (𝑧 < 𝐵 ↔ (𝐵 − 1) < 𝐵)) |
20 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝐵 − 1) → (𝑧 < 𝑦 ↔ (𝐵 − 1) < 𝑦)) |
21 | 20 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝐵 − 1) → (∃𝑦 ∈ 𝐴 𝑧 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦)) |
22 | 19, 21 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐵 − 1) → ((𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) ↔ ((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦))) |
23 | 22 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 − 1) ∈ ℝ
→ (∀𝑧 ∈
ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → ((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦))) |
24 | 18, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℝ →
(∀𝑧 ∈ ℝ
(𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → ((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦))) |
25 | 24 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑧 ∈
ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → ((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦))) |
26 | | ltm1 10863 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) < 𝐵) |
27 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦) → ((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦)) |
28 | 26, 27 | syl5com 31 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℝ → (((𝐵 − 1) < 𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦) → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦)) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
→ (((𝐵 − 1) <
𝐵 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦) → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦)) |
30 | 18 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → (𝐵 − 1) ∈ ℝ) |
31 | | mnflt 11957 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 − 1) ∈ ℝ
→ -∞ < (𝐵
− 1)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → -∞ < (𝐵 − 1)) |
33 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 − 1) ∈ ℝ
→ (𝐵 − 1) ∈
ℝ*) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → (𝐵 − 1) ∈
ℝ*) |
35 | | ssel2 3598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
36 | 35 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
37 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . . . 20
⊢ -∞
∈ ℝ* |
38 | | xrlttr 11973 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((-∞ ∈ ℝ* ∧ (𝐵 − 1) ∈ ℝ* ∧
𝑦 ∈
ℝ*) → ((-∞ < (𝐵 − 1) ∧ (𝐵 − 1) < 𝑦) → -∞ < 𝑦)) |
39 | 37, 38 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 − 1) ∈
ℝ* ∧ 𝑦
∈ ℝ*) → ((-∞ < (𝐵 − 1) ∧ (𝐵 − 1) < 𝑦) → -∞ < 𝑦)) |
40 | 34, 36, 39 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → ((-∞ < (𝐵 − 1) ∧ (𝐵 − 1) < 𝑦) → -∞ < 𝑦)) |
41 | 32, 40 | mpand 711 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → ((𝐵 − 1) < 𝑦 → -∞ < 𝑦)) |
42 | 41 | reximdva 3017 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∃𝑦 ∈
𝐴 (𝐵 − 1) < 𝑦 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
43 | 25, 29, 42 | 3syld 60 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑧 ∈
ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
44 | 43 | a1dd 50 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑧 ∈
ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦))) |
45 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
46 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 1 → (𝑧 < 𝐵 ↔ 1 < 𝐵)) |
47 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 1 → (𝑧 < 𝑦 ↔ 1 < 𝑦)) |
48 | 47 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 1 → (∃𝑦 ∈ 𝐴 𝑧 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 1 < 𝑦)) |
49 | 46, 48 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 1 → ((𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) ↔ (1 < 𝐵 → ∃𝑦 ∈ 𝐴 1 < 𝑦))) |
50 | 49 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℝ → (∀𝑧
∈ ℝ (𝑧 <
𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (1 < 𝐵 → ∃𝑦 ∈ 𝐴 1 < 𝑦))) |
51 | 45, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (1 < 𝐵 → ∃𝑦 ∈ 𝐴 1 < 𝑦)) |
52 | | ltpnf 11954 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) |
53 | 45, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ |
54 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 = +∞ → (1 < 𝐵 ↔ 1 <
+∞)) |
55 | 53, 54 | mpbiri 248 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = +∞ → 1 < 𝐵) |
56 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 <
𝐵 → ∃𝑦 ∈ 𝐴 1 < 𝑦) → (1 < 𝐵 → ∃𝑦 ∈ 𝐴 1 < 𝑦)) |
57 | 55, 56 | syl5com 31 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = +∞ → ((1 <
𝐵 → ∃𝑦 ∈ 𝐴 1 < 𝑦) → ∃𝑦 ∈ 𝐴 1 < 𝑦)) |
58 | | mnflt 11957 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℝ → -∞ < 1) |
59 | 45, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ -∞
< 1 |
60 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) |
61 | 45, 60 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
62 | | xrlttr 11973 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((-∞ ∈ ℝ* ∧ 1 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((-∞ < 1 ∧ 1 < 𝑦) → -∞ < 𝑦)) |
63 | 37, 61, 62 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ*
→ ((-∞ < 1 ∧ 1 < 𝑦) → -∞ < 𝑦)) |
64 | 59, 63 | mpani 712 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ*
→ (1 < 𝑦 →
-∞ < 𝑦)) |
65 | 35, 64 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → (1 < 𝑦 → -∞ < 𝑦)) |
66 | 65 | reximdva 3017 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ⊆ ℝ*
→ (∃𝑦 ∈
𝐴 1 < 𝑦 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
67 | 57, 66 | sylan9r 690 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 = +∞) →
((1 < 𝐵 →
∃𝑦 ∈ 𝐴 1 < 𝑦) → ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
68 | 51, 67 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 = +∞) →
(∀𝑧 ∈ ℝ
(𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
69 | 68 | a1dd 50 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 = +∞) →
(∀𝑧 ∈ ℝ
(𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦))) |
70 | | xrltnr 11953 |
. . . . . . . . . . . . . . . . . . 19
⊢ (-∞
∈ ℝ* → ¬ -∞ <
-∞) |
71 | 37, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
-∞ < -∞ |
72 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = -∞ → (-∞
< 𝐵 ↔ -∞ <
-∞)) |
73 | 71, 72 | mtbiri 317 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = -∞ → ¬
-∞ < 𝐵) |
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 = -∞) →
¬ -∞ < 𝐵) |
75 | 74 | pm2.21d 118 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 = -∞) →
(-∞ < 𝐵 →
∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
76 | 75 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 = -∞) →
(∀𝑧 ∈ ℝ
(𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦))) |
77 | 44, 69, 76 | 3jaodan 1394 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ*
∧ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 = -∞)) →
(∀𝑧 ∈ ℝ
(𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦))) |
78 | 17, 77 | sylan2b 492 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) → (∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦))) |
79 | 78 | imp 445 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
80 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑥 = -∞ → (𝑥 < 𝐵 ↔ -∞ < 𝐵)) |
81 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢ (𝑥 = -∞ → (𝑥 < 𝑦 ↔ -∞ < 𝑦)) |
82 | 81 | rexbidv 3052 |
. . . . . . . . . . . 12
⊢ (𝑥 = -∞ → (∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 -∞ < 𝑦)) |
83 | 80, 82 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑥 = -∞ → ((𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) ↔ (-∞ < 𝐵 → ∃𝑦 ∈ 𝐴 -∞ < 𝑦))) |
84 | 79, 83 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (𝑥 = -∞ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
85 | 84 | a1dd 50 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (𝑥 = -∞ → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
86 | 8, 16, 85 | 3jaod 1392 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → ((𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞) → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
87 | 6, 86 | syl5bi 232 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (𝑥 ∈ ℝ* → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
88 | 87 | com23 86 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → ((𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 ∈ ℝ* → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
89 | 88 | ralimdv2 2961 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
90 | 89 | ex 450 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) → (∀𝑧 ∈ ℝ (𝑧 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
91 | 5, 90 | syl5bi 232 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))) |
92 | 91 | pm2.43d 53 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
93 | | rexr 10085 |
. . . 4
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
94 | 93 | imim1i 63 |
. . 3
⊢ ((𝑥 ∈ ℝ*
→ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) → (𝑥 ∈ ℝ → (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |
95 | 94 | ralimi2 2949 |
. 2
⊢
(∀𝑥 ∈
ℝ* (𝑥 <
𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) |
96 | 92, 95 | impbid1 215 |
1
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ∈
ℝ*) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) ↔ ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) |