| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | peano2re 11435 | . . . . . . . . 9
⊢ (𝑤 ∈ ℝ → (𝑤 + 1) ∈
ℝ) | 
| 2 | 1 | adantl 481 | . . . . . . . 8
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ) → (𝑤 + 1) ∈ ℝ) | 
| 3 |  | simpl 482 | . . . . . . . 8
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | 
| 4 |  | breq1 5145 | . . . . . . . . . 10
⊢ (𝑥 = (𝑤 + 1) → (𝑥 ≤ 𝑦 ↔ (𝑤 + 1) ≤ 𝑦)) | 
| 5 | 4 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑥 = (𝑤 + 1) → (∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦)) | 
| 6 | 5 | rspcva 3619 | . . . . . . . 8
⊢ (((𝑤 + 1) ∈ ℝ ∧
∀𝑥 ∈ ℝ
∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦) | 
| 7 | 2, 3, 6 | syl2anc 584 | . . . . . . 7
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ) → ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦) | 
| 8 | 7 | adantll 714 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → ∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦) | 
| 9 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑦 𝐴 ⊆
ℝ* | 
| 10 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑦ℝ | 
| 11 |  | nfre1 3284 | . . . . . . . . . 10
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 | 
| 12 | 10, 11 | nfralw 3310 | . . . . . . . . 9
⊢
Ⅎ𝑦∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 | 
| 13 | 9, 12 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑦(𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) | 
| 14 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑦 𝑤 ∈ ℝ | 
| 15 | 13, 14 | nfan 1898 | . . . . . . 7
⊢
Ⅎ𝑦((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) | 
| 16 |  | simp1r 1198 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 ∈ ℝ) | 
| 17 |  | rexr 11308 | . . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ → 𝑤 ∈
ℝ*) | 
| 18 | 16, 17 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 ∈ ℝ*) | 
| 19 | 1 | rexrd 11312 | . . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ → (𝑤 + 1) ∈
ℝ*) | 
| 20 | 16, 19 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → (𝑤 + 1) ∈
ℝ*) | 
| 21 |  | simp1l 1197 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝐴 ⊆
ℝ*) | 
| 22 |  | simp2 1137 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑦 ∈ 𝐴) | 
| 23 |  | ssel2 3977 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) | 
| 24 | 21, 22, 23 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑦 ∈ ℝ*) | 
| 25 | 16 | ltp1d 12199 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 < (𝑤 + 1)) | 
| 26 |  | simp3 1138 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → (𝑤 + 1) ≤ 𝑦) | 
| 27 | 18, 20, 24, 25, 26 | xrltletrd 13204 | . . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
∧ 𝑦 ∈ 𝐴 ∧ (𝑤 + 1) ≤ 𝑦) → 𝑤 < 𝑦) | 
| 28 | 27 | 3exp 1119 | . . . . . . . 8
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑤 ∈ ℝ)
→ (𝑦 ∈ 𝐴 → ((𝑤 + 1) ≤ 𝑦 → 𝑤 < 𝑦))) | 
| 29 | 28 | adantlr 715 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → (𝑦 ∈ 𝐴 → ((𝑤 + 1) ≤ 𝑦 → 𝑤 < 𝑦))) | 
| 30 | 15, 29 | reximdai 3260 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → (∃𝑦 ∈ 𝐴 (𝑤 + 1) ≤ 𝑦 → ∃𝑦 ∈ 𝐴 𝑤 < 𝑦)) | 
| 31 | 8, 30 | mpd 15 | . . . . 5
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑤 < 𝑦) | 
| 32 | 31 | ralrimiva 3145 | . . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦) → ∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑤 < 𝑦) | 
| 33 | 32 | ex 412 | . . 3
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 → ∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑤 < 𝑦)) | 
| 34 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 < 𝑦 ↔ 𝑥 < 𝑦)) | 
| 35 | 34 | rexbidv 3178 | . . . . . . 7
⊢ (𝑤 = 𝑥 → (∃𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) | 
| 36 | 35 | cbvralvw 3236 | . . . . . 6
⊢
(∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) | 
| 37 | 36 | biimpi 216 | . . . . 5
⊢
(∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) | 
| 38 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑥 𝐴 ⊆
ℝ* | 
| 39 |  | nfra1 3283 | . . . . . . 7
⊢
Ⅎ𝑥∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 | 
| 40 | 38, 39 | nfan 1898 | . . . . . 6
⊢
Ⅎ𝑥(𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) | 
| 41 |  | simpll 766 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → 𝐴 ⊆
ℝ*) | 
| 42 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) | 
| 43 |  | rspa 3247 | . . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) | 
| 44 | 43 | adantll 714 | . . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) | 
| 45 |  | rexr 11308 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 46 | 45 | ad3antlr 731 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ*) | 
| 47 | 23 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ*) | 
| 48 | 47 | adantllr 719 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ*) | 
| 49 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) | 
| 50 | 46, 48, 49 | xrltled 13193 | . . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) ∧ 𝑥 < 𝑦) → 𝑥 ≤ 𝑦) | 
| 51 | 50 | ex 412 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ 𝑦 ∈ 𝐴) → (𝑥 < 𝑦 → 𝑥 ≤ 𝑦)) | 
| 52 | 51 | reximdva 3167 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
→ (∃𝑦 ∈
𝐴 𝑥 < 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | 
| 53 | 52 | adantlr 715 | . . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | 
| 54 | 44, 53 | mpd 15 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | 
| 55 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | 
| 56 | 41, 42, 54, 55 | syl21anc 837 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | 
| 57 | 56 | ex 412 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → (𝑥 ∈ ℝ → ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | 
| 58 | 40, 57 | ralrimi 3256 | . . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | 
| 59 | 37, 58 | sylan2 593 | . . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | 
| 60 | 59 | ex 412 | . . 3
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | 
| 61 | 33, 60 | impbid 212 | . 2
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ↔ ∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑤 < 𝑦)) | 
| 62 |  | supxrunb2 13363 | . 2
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑤 ∈
ℝ ∃𝑦 ∈
𝐴 𝑤 < 𝑦 ↔ sup(𝐴, ℝ*, < ) =
+∞)) | 
| 63 | 61, 62 | bitrd 279 | 1
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |