Step | Hyp | Ref
| Expression |
1 | | mopni.1 |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
2 | 1 | mopnuni 22246 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
3 | 2 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝑋 = ∪
𝐽) |
4 | 3 | difeq1d 3727 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑋 ∖ 𝑆) = (∪ 𝐽 ∖ 𝑆)) |
5 | | difssd 3738 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑋 ∖ 𝑆) ⊆ 𝑋) |
6 | | simpl3 1066 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → 𝑅 ∈
ℝ*) |
7 | | simpl1 1064 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → 𝐷 ∈ (∞Met‘𝑋)) |
8 | | simpl2 1065 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → 𝑃 ∈ 𝑋) |
9 | | eldifi 3732 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ 𝑆) → 𝑦 ∈ 𝑋) |
10 | 9 | adantl 482 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → 𝑦 ∈ 𝑋) |
11 | | xmetcl 22136 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑃𝐷𝑦) ∈
ℝ*) |
12 | 7, 8, 10, 11 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → (𝑃𝐷𝑦) ∈
ℝ*) |
13 | | eldif 3584 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑋 ∖ 𝑆) ↔ (𝑦 ∈ 𝑋 ∧ ¬ 𝑦 ∈ 𝑆)) |
14 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (𝑃𝐷𝑧) = (𝑃𝐷𝑦)) |
15 | 14 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷𝑦) ≤ 𝑅)) |
16 | | blcld.3 |
. . . . . . . . . . . . 13
⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} |
17 | 15, 16 | elrab2 3366 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ (𝑃𝐷𝑦) ≤ 𝑅)) |
18 | 17 | simplbi2 655 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑋 → ((𝑃𝐷𝑦) ≤ 𝑅 → 𝑦 ∈ 𝑆)) |
19 | 18 | con3dimp 457 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑋 ∧ ¬ 𝑦 ∈ 𝑆) → ¬ (𝑃𝐷𝑦) ≤ 𝑅) |
20 | 13, 19 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ 𝑆) → ¬ (𝑃𝐷𝑦) ≤ 𝑅) |
21 | 20 | adantl 482 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → ¬ (𝑃𝐷𝑦) ≤ 𝑅) |
22 | | xrltnle 10105 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ*
∧ (𝑃𝐷𝑦) ∈ ℝ*) → (𝑅 < (𝑃𝐷𝑦) ↔ ¬ (𝑃𝐷𝑦) ≤ 𝑅)) |
23 | 6, 12, 22 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → (𝑅 < (𝑃𝐷𝑦) ↔ ¬ (𝑃𝐷𝑦) ≤ 𝑅)) |
24 | 21, 23 | mpbird 247 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → 𝑅 < (𝑃𝐷𝑦)) |
25 | | qbtwnxr 12031 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ*
∧ (𝑃𝐷𝑦) ∈ ℝ* ∧ 𝑅 < (𝑃𝐷𝑦)) → ∃𝑥 ∈ ℚ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦))) |
26 | 6, 12, 24, 25 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → ∃𝑥 ∈ ℚ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦))) |
27 | | qre 11793 |
. . . . . . . 8
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
28 | 7 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝐷 ∈ (∞Met‘𝑋)) |
29 | 10 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑦 ∈ 𝑋) |
30 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑃𝐷𝑦) ∈
ℝ*) |
31 | | rexr 10085 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
32 | 31 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑥 ∈ ℝ*) |
33 | 32 | xnegcld 12130 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → -𝑒𝑥 ∈
ℝ*) |
34 | 30, 33 | xaddcld 12131 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
∈ ℝ*) |
35 | | blelrn 22222 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
∈ ℝ*) → (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∈ ran (ball‘𝐷)) |
36 | 28, 29, 34, 35 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∈ ran (ball‘𝐷)) |
37 | | simprrr 805 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑥 < (𝑃𝐷𝑦)) |
38 | | xposdif 12092 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ (𝑃𝐷𝑦) ∈ ℝ*) → (𝑥 < (𝑃𝐷𝑦) ↔ 0 < ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) |
39 | 32, 30, 38 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑥 < (𝑃𝐷𝑦) ↔ 0 < ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) |
40 | 37, 39 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 0 < ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)) |
41 | | xblcntr 22216 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
∈ ℝ* ∧ 0 < ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)))
→ 𝑦 ∈ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) |
42 | 28, 29, 34, 40, 41 | syl112anc 1330 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑦 ∈ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) |
43 | | incom 3805 |
. . . . . . . . . . . . 13
⊢ ((𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∩ (𝑃(ball‘𝐷)𝑥)) = ((𝑃(ball‘𝐷)𝑥) ∩ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) |
44 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑃 ∈ 𝑋) |
45 | | xaddcom 12071 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
∈ ℝ*) → (𝑥 +𝑒 ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)) =
(((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
+𝑒 𝑥)) |
46 | 32, 34, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑥 +𝑒 ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)) =
(((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
+𝑒 𝑥)) |
47 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑥 ∈ ℝ) |
48 | | xnpcan 12082 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃𝐷𝑦) ∈ ℝ* ∧ 𝑥 ∈ ℝ) → (((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
+𝑒 𝑥) =
(𝑃𝐷𝑦)) |
49 | 30, 47, 48 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
+𝑒 𝑥) =
(𝑃𝐷𝑦)) |
50 | 46, 49 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑥 +𝑒 ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)) =
(𝑃𝐷𝑦)) |
51 | | xrleid 11983 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃𝐷𝑦) ∈ ℝ* → (𝑃𝐷𝑦) ≤ (𝑃𝐷𝑦)) |
52 | 30, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑃𝐷𝑦) ≤ (𝑃𝐷𝑦)) |
53 | 50, 52 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑥 +𝑒 ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
≤ (𝑃𝐷𝑦)) |
54 | | bldisj 22203 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥 ∈ ℝ* ∧ ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
∈ ℝ* ∧ (𝑥 +𝑒 ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
≤ (𝑃𝐷𝑦))) → ((𝑃(ball‘𝐷)𝑥) ∩ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) =
∅) |
55 | 28, 44, 29, 32, 34, 53, 54 | syl33anc 1341 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → ((𝑃(ball‘𝐷)𝑥) ∩ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))) =
∅) |
56 | 43, 55 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → ((𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∩ (𝑃(ball‘𝐷)𝑥)) = ∅) |
57 | | blssm 22223 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ ((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)
∈ ℝ*) → (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ 𝑋) |
58 | 28, 29, 34, 57 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ 𝑋) |
59 | | reldisj 4020 |
. . . . . . . . . . . . 13
⊢ ((𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ 𝑋 → (((𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∩ (𝑃(ball‘𝐷)𝑥)) = ∅ ↔ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ (𝑃(ball‘𝐷)𝑥)))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (((𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∩ (𝑃(ball‘𝐷)𝑥)) = ∅ ↔ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ (𝑃(ball‘𝐷)𝑥)))) |
61 | 56, 60 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ (𝑃(ball‘𝐷)𝑥))) |
62 | 6 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑅 ∈
ℝ*) |
63 | | simprrl 804 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑅 < 𝑥) |
64 | 1, 16 | blsscls2 22309 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℝ*
∧ 𝑅 < 𝑥)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑥)) |
65 | 28, 44, 62, 32, 63, 64 | syl23anc 1333 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑥)) |
66 | 65 | sscond 3747 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑋 ∖ (𝑃(ball‘𝐷)𝑥)) ⊆ (𝑋 ∖ 𝑆)) |
67 | 61, 66 | sstrd 3613 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ 𝑆)) |
68 | | eleq2 2690 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
→ (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥)))) |
69 | | sseq1 3626 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
→ (𝑤 ⊆ (𝑋 ∖ 𝑆) ↔ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ 𝑆))) |
70 | 68, 69 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
→ ((𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆)) ↔ (𝑦 ∈ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∧ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ 𝑆)))) |
71 | 70 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∈ ran (ball‘𝐷)
∧ (𝑦 ∈ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
∧ (𝑦(ball‘𝐷)((𝑃𝐷𝑦) +𝑒
-𝑒𝑥))
⊆ (𝑋 ∖ 𝑆))) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆))) |
72 | 36, 42, 67, 71 | syl12anc 1324 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ (𝑥 ∈ ℝ ∧ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)))) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆))) |
73 | 72 | expr 643 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ 𝑥 ∈ ℝ) → ((𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆)))) |
74 | 27, 73 | sylan2 491 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) ∧ 𝑥 ∈ ℚ) → ((𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆)))) |
75 | 74 | rexlimdva 3031 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → (∃𝑥 ∈ ℚ (𝑅 < 𝑥 ∧ 𝑥 < (𝑃𝐷𝑦)) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆)))) |
76 | 26, 75 | mpd 15 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ (𝑋 ∖ 𝑆)) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆))) |
77 | 76 | ralrimiva 2966 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) →
∀𝑦 ∈ (𝑋 ∖ 𝑆)∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆))) |
78 | 1 | elmopn 22247 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → ((𝑋 ∖ 𝑆) ∈ 𝐽 ↔ ((𝑋 ∖ 𝑆) ⊆ 𝑋 ∧ ∀𝑦 ∈ (𝑋 ∖ 𝑆)∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆))))) |
79 | 78 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((𝑋 ∖ 𝑆) ∈ 𝐽 ↔ ((𝑋 ∖ 𝑆) ⊆ 𝑋 ∧ ∀𝑦 ∈ (𝑋 ∖ 𝑆)∃𝑤 ∈ ran (ball‘𝐷)(𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑋 ∖ 𝑆))))) |
80 | 5, 77, 79 | mpbir2and 957 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑋 ∖ 𝑆) ∈ 𝐽) |
81 | 4, 80 | eqeltrrd 2702 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
82 | 1 | mopntop 22245 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
83 | 82 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝐽 ∈ Top) |
84 | | ssrab2 3687 |
. . . . 5
⊢ {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ 𝑋 |
85 | 16, 84 | eqsstri 3635 |
. . . 4
⊢ 𝑆 ⊆ 𝑋 |
86 | 85, 3 | syl5sseq 3653 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝑆 ⊆ ∪ 𝐽) |
87 | | eqid 2622 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
88 | 87 | iscld2 20832 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ (𝑆 ∈
(Clsd‘𝐽) ↔
(∪ 𝐽 ∖ 𝑆) ∈ 𝐽)) |
89 | 83, 86, 88 | syl2anc 693 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑆 ∈ (Clsd‘𝐽) ↔ (∪ 𝐽
∖ 𝑆) ∈ 𝐽)) |
90 | 81, 89 | mpbird 247 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝑆 ∈ (Clsd‘𝐽)) |