| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssel 3977 | . . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ (𝑧 ∈ 𝐴 → 𝑧 ∈
ℝ*)) | 
| 2 |  | pnfnlt 13170 | . . . . . . . 8
⊢ (𝑧 ∈ ℝ*
→ ¬ +∞ < 𝑧) | 
| 3 | 1, 2 | syl6 35 | . . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ (𝑧 ∈ 𝐴 → ¬ +∞ <
𝑧)) | 
| 4 | 3 | ralrimiv 3145 | . . . . . 6
⊢ (𝐴 ⊆ ℝ*
→ ∀𝑧 ∈
𝐴 ¬ +∞ < 𝑧) | 
| 5 | 4 | adantr 480 | . . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → ∀𝑧 ∈ 𝐴 ¬ +∞ < 𝑧) | 
| 6 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑥 < 𝑦 ↔ 𝑧 < 𝑦)) | 
| 7 | 6 | rexbidv 3179 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) | 
| 8 | 7 | rspcva 3620 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ∧
∀𝑥 ∈ ℝ
∃𝑦 ∈ 𝐴 𝑥 < 𝑦) → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦) | 
| 9 | 8 | adantrr 717 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧
(∀𝑥 ∈ ℝ
∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ∧ 𝐴 ⊆ ℝ*)) →
∃𝑦 ∈ 𝐴 𝑧 < 𝑦) | 
| 10 | 9 | ancoms 458 | . . . . . . . . . . 11
⊢
(((∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 ∧ 𝐴 ⊆ ℝ*) ∧ 𝑧 ∈ ℝ) →
∃𝑦 ∈ 𝐴 𝑧 < 𝑦) | 
| 11 | 10 | exp31 419 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 → (𝐴 ⊆ ℝ* → (𝑧 ∈ ℝ →
∃𝑦 ∈ 𝐴 𝑧 < 𝑦))) | 
| 12 | 11 | a1dd 50 | . . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 → (𝐴 ⊆ ℝ* → (𝑧 < +∞ → (𝑧 ∈ ℝ →
∃𝑦 ∈ 𝐴 𝑧 < 𝑦)))) | 
| 13 | 12 | com4r 94 | . . . . . . . 8
⊢ (𝑧 ∈ ℝ →
(∀𝑥 ∈ ℝ
∃𝑦 ∈ 𝐴 𝑥 < 𝑦 → (𝐴 ⊆ ℝ* → (𝑧 < +∞ →
∃𝑦 ∈ 𝐴 𝑧 < 𝑦)))) | 
| 14 | 13 | com13 88 | . . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 → (𝑧 ∈ ℝ → (𝑧 < +∞ → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)))) | 
| 15 | 14 | imp 406 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → (𝑧 ∈ ℝ → (𝑧 < +∞ → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦))) | 
| 16 | 15 | ralrimiv 3145 | . . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → ∀𝑧 ∈ ℝ (𝑧 < +∞ → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦)) | 
| 17 | 5, 16 | jca 511 | . . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → (∀𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀𝑧 ∈ ℝ (𝑧 < +∞ → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦))) | 
| 18 |  | pnfxr 11315 | . . . . 5
⊢ +∞
∈ ℝ* | 
| 19 |  | supxr 13355 | . . . . 5
⊢ (((𝐴 ⊆ ℝ*
∧ +∞ ∈ ℝ*) ∧ (∀𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀𝑧 ∈ ℝ (𝑧 < +∞ → ∃𝑦 ∈ 𝐴 𝑧 < 𝑦))) → sup(𝐴, ℝ*, < ) =
+∞) | 
| 20 | 18, 19 | mpanl2 701 | . . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ (∀𝑧 ∈
𝐴 ¬ +∞ < 𝑧 ∧ ∀𝑧 ∈ ℝ (𝑧 < +∞ →
∃𝑦 ∈ 𝐴 𝑧 < 𝑦))) → sup(𝐴, ℝ*, < ) =
+∞) | 
| 21 | 17, 20 | syldan 591 | . . 3
⊢ ((𝐴 ⊆ ℝ*
∧ ∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦) → sup(𝐴, ℝ*, < ) =
+∞) | 
| 22 | 21 | ex 412 | . 2
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 → sup(𝐴, ℝ*, < ) =
+∞)) | 
| 23 |  | rexr 11307 | . . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 24 | 23 | ad2antlr 727 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ sup(𝐴,
ℝ*, < ) = +∞) → 𝑥 ∈ ℝ*) | 
| 25 |  | ltpnf 13162 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) | 
| 26 |  | breq2 5147 | . . . . . . . . 9
⊢
(sup(𝐴,
ℝ*, < ) = +∞ → (𝑥 < sup(𝐴, ℝ*, < ) ↔ 𝑥 <
+∞)) | 
| 27 | 25, 26 | imbitrrid 246 | . . . . . . . 8
⊢
(sup(𝐴,
ℝ*, < ) = +∞ → (𝑥 ∈ ℝ → 𝑥 < sup(𝐴, ℝ*, <
))) | 
| 28 | 27 | impcom 407 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ sup(𝐴, ℝ*, < ) =
+∞) → 𝑥 <
sup(𝐴, ℝ*,
< )) | 
| 29 | 28 | adantll 714 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ sup(𝐴,
ℝ*, < ) = +∞) → 𝑥 < sup(𝐴, ℝ*, <
)) | 
| 30 |  | xrltso 13183 | . . . . . . . 8
⊢  < Or
ℝ* | 
| 31 | 30 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ sup(𝐴,
ℝ*, < ) = +∞) → < Or
ℝ*) | 
| 32 |  | xrsupss 13351 | . . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑧 ∈
ℝ* (∀𝑤 ∈ 𝐴 ¬ 𝑧 < 𝑤 ∧ ∀𝑤 ∈ ℝ* (𝑤 < 𝑧 → ∃𝑦 ∈ 𝐴 𝑤 < 𝑦))) | 
| 33 | 32 | ad2antrr 726 | . . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ sup(𝐴,
ℝ*, < ) = +∞) → ∃𝑧 ∈ ℝ* (∀𝑤 ∈ 𝐴 ¬ 𝑧 < 𝑤 ∧ ∀𝑤 ∈ ℝ* (𝑤 < 𝑧 → ∃𝑦 ∈ 𝐴 𝑤 < 𝑦))) | 
| 34 | 31, 33 | suplub 9500 | . . . . . 6
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ sup(𝐴,
ℝ*, < ) = +∞) → ((𝑥 ∈ ℝ* ∧ 𝑥 < sup(𝐴, ℝ*, < )) →
∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) | 
| 35 | 24, 29, 34 | mp2and 699 | . . . . 5
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ ℝ)
∧ sup(𝐴,
ℝ*, < ) = +∞) → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) | 
| 36 | 35 | exp31 419 | . . . 4
⊢ (𝐴 ⊆ ℝ*
→ (𝑥 ∈ ℝ
→ (sup(𝐴,
ℝ*, < ) = +∞ → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) | 
| 37 | 36 | com23 86 | . . 3
⊢ (𝐴 ⊆ ℝ*
→ (sup(𝐴,
ℝ*, < ) = +∞ → (𝑥 ∈ ℝ → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) | 
| 38 | 37 | ralrimdv 3152 | . 2
⊢ (𝐴 ⊆ ℝ*
→ (sup(𝐴,
ℝ*, < ) = +∞ → ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)) | 
| 39 | 22, 38 | impbid 212 | 1
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑥 ∈
ℝ ∃𝑦 ∈
𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |