Proof of Theorem ssblex
| Step | Hyp | Ref
| Expression |
| 1 | | simprl 771 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ 𝑅 ∈
ℝ+) |
| 2 | 1 | rphalfcld 13089 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ (𝑅 / 2) ∈
ℝ+) |
| 3 | | simprr 773 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ 𝑆 ∈
ℝ+) |
| 4 | 2, 3 | ifcld 4572 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) ∈
ℝ+) |
| 5 | 4 | rpred 13077 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) ∈ ℝ) |
| 6 | 2 | rpred 13077 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ (𝑅 / 2) ∈
ℝ) |
| 7 | 1 | rpred 13077 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ 𝑅 ∈
ℝ) |
| 8 | 3 | rpred 13077 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ 𝑆 ∈
ℝ) |
| 9 | | min1 13231 |
. . . 4
⊢ (((𝑅 / 2) ∈ ℝ ∧ 𝑆 ∈ ℝ) →
if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) ≤ (𝑅 / 2)) |
| 10 | 6, 8, 9 | syl2anc 584 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) ≤ (𝑅 / 2)) |
| 11 | 1 | rpgt0d 13080 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ 0 < 𝑅) |
| 12 | | halfpos 12496 |
. . . . 5
⊢ (𝑅 ∈ ℝ → (0 <
𝑅 ↔ (𝑅 / 2) < 𝑅)) |
| 13 | 7, 12 | syl 17 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ (0 < 𝑅 ↔
(𝑅 / 2) < 𝑅)) |
| 14 | 11, 13 | mpbid 232 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ (𝑅 / 2) < 𝑅) |
| 15 | 5, 6, 7, 10, 14 | lelttrd 11419 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) < 𝑅) |
| 16 | | simpl 482 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ (𝐷 ∈
(∞Met‘𝑋) ∧
𝑃 ∈ 𝑋)) |
| 17 | 4 | rpxrd 13078 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) ∈
ℝ*) |
| 18 | 3 | rpxrd 13078 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ 𝑆 ∈
ℝ*) |
| 19 | | min2 13232 |
. . . 4
⊢ (((𝑅 / 2) ∈ ℝ ∧ 𝑆 ∈ ℝ) →
if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) ≤ 𝑆) |
| 20 | 6, 8, 19 | syl2anc 584 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) ≤ 𝑆) |
| 21 | | ssbl 24433 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) ∈ ℝ* ∧ 𝑆 ∈ ℝ*)
∧ if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) ≤ 𝑆) → (𝑃(ball‘𝐷)if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆)) ⊆ (𝑃(ball‘𝐷)𝑆)) |
| 22 | 16, 17, 18, 20, 21 | syl121anc 1377 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ (𝑃(ball‘𝐷)if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆)) ⊆ (𝑃(ball‘𝐷)𝑆)) |
| 23 | | breq1 5146 |
. . . 4
⊢ (𝑥 = if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) → (𝑥 < 𝑅 ↔ if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) < 𝑅)) |
| 24 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) → (𝑃(ball‘𝐷)𝑥) = (𝑃(ball‘𝐷)if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆))) |
| 25 | 24 | sseq1d 4015 |
. . . 4
⊢ (𝑥 = if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) → ((𝑃(ball‘𝐷)𝑥) ⊆ (𝑃(ball‘𝐷)𝑆) ↔ (𝑃(ball‘𝐷)if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆)) ⊆ (𝑃(ball‘𝐷)𝑆))) |
| 26 | 23, 25 | anbi12d 632 |
. . 3
⊢ (𝑥 = if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) → ((𝑥 < 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ (𝑃(ball‘𝐷)𝑆)) ↔ (if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) < 𝑅 ∧ (𝑃(ball‘𝐷)if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆)) ⊆ (𝑃(ball‘𝐷)𝑆)))) |
| 27 | 26 | rspcev 3622 |
. 2
⊢
((if((𝑅 / 2) ≤
𝑆, (𝑅 / 2), 𝑆) ∈ ℝ+ ∧
(if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆) < 𝑅 ∧ (𝑃(ball‘𝐷)if((𝑅 / 2) ≤ 𝑆, (𝑅 / 2), 𝑆)) ⊆ (𝑃(ball‘𝐷)𝑆))) → ∃𝑥 ∈ ℝ+ (𝑥 < 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ (𝑃(ball‘𝐷)𝑆))) |
| 28 | 4, 15, 22, 27 | syl12anc 837 |
1
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ ∃𝑥 ∈
ℝ+ (𝑥 <
𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ (𝑃(ball‘𝐷)𝑆))) |