Proof of Theorem metss2lem
| Step | Hyp | Ref
| Expression |
| 1 | | metss2.2 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
| 2 | 1 | ad2antrr 488 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝐷 ∈ (Met‘𝑋)) |
| 3 | | simplrl 535 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 4 | | simpr 110 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 5 | | metcl 14589 |
. . . . . 6
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ∈ ℝ) |
| 6 | 2, 3, 4, 5 | syl3anc 1249 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ∈ ℝ) |
| 7 | | simplrr 536 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈
ℝ+) |
| 8 | 7 | rpred 9771 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈ ℝ) |
| 9 | | metss2.3 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
| 10 | 9 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑅 ∈
ℝ+) |
| 11 | 6, 8, 10 | ltmuldiv2d 9820 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 · (𝑥𝐷𝑦)) < 𝑆 ↔ (𝑥𝐷𝑦) < (𝑆 / 𝑅))) |
| 12 | | metss2.4 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) |
| 13 | 12 | anassrs 400 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) |
| 14 | 13 | adantlrr 483 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) |
| 15 | | metss2.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) |
| 16 | 15 | ad2antrr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝐶 ∈ (Met‘𝑋)) |
| 17 | | metcl 14589 |
. . . . . . 7
⊢ ((𝐶 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ ℝ) |
| 18 | 16, 3, 4, 17 | syl3anc 1249 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ ℝ) |
| 19 | 10 | rpred 9771 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑅 ∈ ℝ) |
| 20 | 19, 6 | remulcld 8057 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑅 · (𝑥𝐷𝑦)) ∈ ℝ) |
| 21 | | lelttr 8115 |
. . . . . 6
⊢ (((𝑥𝐶𝑦) ∈ ℝ ∧ (𝑅 · (𝑥𝐷𝑦)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (((𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)) ∧ (𝑅 · (𝑥𝐷𝑦)) < 𝑆) → (𝑥𝐶𝑦) < 𝑆)) |
| 22 | 18, 20, 8, 21 | syl3anc 1249 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)) ∧ (𝑅 · (𝑥𝐷𝑦)) < 𝑆) → (𝑥𝐶𝑦) < 𝑆)) |
| 23 | 14, 22 | mpand 429 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 · (𝑥𝐷𝑦)) < 𝑆 → (𝑥𝐶𝑦) < 𝑆)) |
| 24 | 11, 23 | sylbird 170 |
. . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) < (𝑆 / 𝑅) → (𝑥𝐶𝑦) < 𝑆)) |
| 25 | 24 | ss2rabdv 3264 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < (𝑆 / 𝑅)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝑥𝐶𝑦) < 𝑆}) |
| 26 | | metxmet 14591 |
. . . . 5
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 27 | 1, 26 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 28 | 27 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 29 | | simprl 529 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝑥 ∈ 𝑋) |
| 30 | | simpr 110 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+) → 𝑆 ∈
ℝ+) |
| 31 | | rpdivcl 9754 |
. . . . 5
⊢ ((𝑆 ∈ ℝ+
∧ 𝑅 ∈
ℝ+) → (𝑆 / 𝑅) ∈
ℝ+) |
| 32 | 30, 9, 31 | syl2anr 290 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑆 / 𝑅) ∈
ℝ+) |
| 33 | 32 | rpxrd 9772 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑆 / 𝑅) ∈
ℝ*) |
| 34 | | blval 14625 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (𝑆 / 𝑅) ∈ ℝ*) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < (𝑆 / 𝑅)}) |
| 35 | 28, 29, 33, 34 | syl3anc 1249 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < (𝑆 / 𝑅)}) |
| 36 | | metxmet 14591 |
. . . . 5
⊢ (𝐶 ∈ (Met‘𝑋) → 𝐶 ∈ (∞Met‘𝑋)) |
| 37 | 15, 36 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋)) |
| 38 | 37 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝐶 ∈ (∞Met‘𝑋)) |
| 39 | | rpxr 9736 |
. . . 4
⊢ (𝑆 ∈ ℝ+
→ 𝑆 ∈
ℝ*) |
| 40 | 39 | ad2antll 491 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝑆 ∈
ℝ*) |
| 41 | | blval 14625 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑥(ball‘𝐶)𝑆) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐶𝑦) < 𝑆}) |
| 42 | 38, 29, 40, 41 | syl3anc 1249 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐶)𝑆) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐶𝑦) < 𝑆}) |
| 43 | 25, 35, 42 | 3sstr4d 3228 |
1
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) |