Step | Hyp | Ref
| Expression |
1 | | peano2re 11148 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ → (𝑤 + 1) ∈
ℝ) |
2 | 1 | adantl 482 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ) → (𝑤 + 1) ∈ ℝ) |
3 | | simpl 483 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
4 | | breq1 5077 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑤 + 1) → (𝑥 ≤ 𝑦 ↔ (𝑤 + 1) ≤ 𝑦)) |
5 | 4 | rexbidv 3226 |
. . . . . . . . 9
⊢ (𝑥 = (𝑤 + 1) → (∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦)) |
6 | 5 | rspcva 3559 |
. . . . . . . 8
⊢ (((𝑤 + 1) ∈ ℝ ∧
∀𝑥 ∈ ℝ
∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦) |
7 | 2, 3, 6 | syl2anc 584 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ) → ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦) |
8 | 7 | adantll 711 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦) |
9 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝐴 ⊆
ℝ* |
10 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑦ℝ |
11 | | nfre1 3239 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 |
12 | 10, 11 | nfralw 3151 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 |
13 | 9, 12 | nfan 1902 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) |
14 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑤 ∈ ℝ |
15 | 13, 14 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑦((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) |
16 | | simp1r 1197 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 ∈ ℝ) |
17 | | rexr 11021 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ → 𝑤 ∈
ℝ*) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 ∈ ℝ*) |
19 | 1 | rexrd 11025 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ → (𝑤 + 1) ∈
ℝ*) |
20 | 16, 19 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → (𝑤 + 1) ∈
ℝ*) |
21 | | simp1l 1196 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝐴 ⊆
ℝ*) |
22 | | simp2 1136 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑦 ∈ 𝐴) |
23 | | ssel2 3916 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
24 | 21, 22, 23 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑦 ∈ ℝ*) |
25 | 16 | ltp1d 11905 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 < (𝑤 + 1)) |
26 | | simp3 1137 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → (𝑤 + 1) ≤ 𝑦) |
27 | 18, 20, 24, 25, 26 | xrltletrd 12895 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 < 𝑦) |
28 | 27 | 3exp 1118 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
→ (𝑦 ∈ 𝐴 → ((𝑤 + 1) ≤ 𝑦 → 𝑤 < 𝑦))) |
29 | 28 | adantlr 712 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → (𝑦 ∈ 𝐴 → ((𝑤 + 1) ≤ 𝑦 → 𝑤 < 𝑦))) |
30 | 15, 29 | reximdai 3244 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → (∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦 → ∃𝑦 ∈ 𝐴 𝑤 < 𝑦)) |
31 | 8, 30 | mpd 15 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑤 < 𝑦) |
32 | 31 | ralrimiva 3103 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) → ∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑤 < 𝑦) |
33 | 32 | ex 413 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 → ∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑤 < 𝑦)) |
34 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 < 𝑦 ↔ 𝑥 < 𝑦)) |
35 | 34 | rexbidv 3226 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (∃𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) |
36 | 35 | cbvralvw 3383 |
. . . . . 6
⊢
(∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) |
37 | 36 | biimpi 215 |
. . . . 5
⊢
(∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) |
38 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 ⊆
ℝ* |
39 | | nfra1 3144 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 |
40 | 38, 39 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) |
41 | | simpll 764 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → 𝐴 ⊆
ℝ*) |
42 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
43 | | rspa 3132 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) |
44 | 43 | adantll 711 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) |
45 | | rexr 11021 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
46 | 45 | ad3antlr 728 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ*) |
47 | 23 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ*) |
48 | 47 | adantllr 716 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ*) |
49 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
50 | 46, 48, 49 | xrltled 12884 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑥 ≤ 𝑦) |
51 | 50 | ex 413 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → (𝑥 < 𝑦 → 𝑥 ≤ 𝑦)) |
52 | 51 | reximdva 3203 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
→ (∃𝑦 ∈
𝐴 𝑥 < 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
53 | 52 | adantlr 712 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
54 | 44, 53 | mpd 15 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
55 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
56 | 41, 42, 54, 55 | syl21anc 835 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
57 | 56 | ex 413 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → (𝑥 ∈ ℝ → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
58 | 40, 57 | ralrimi 3141 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
59 | 37, 58 | sylan2 593 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
60 | 59 | ex 413 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
61 | 33, 60 | impbid 211 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ↔ ∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑤 < 𝑦)) |
62 | | supxrunb2 13054 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
63 | 61, 62 | bitrd 278 |
1
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |