Proof of Theorem lpbl
Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (∞Met‘𝑋)) |
2 | | mopni.1 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘𝐷) |
3 | 2 | mopntop 22245 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝐽 ∈ Top) |
5 | | simpl2 1065 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑆 ⊆ 𝑋) |
6 | 2 | mopnuni 22246 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
7 | 1, 6 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑋 = ∪
𝐽) |
8 | 5, 7 | sseqtrd 3641 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑆 ⊆ ∪ 𝐽) |
9 | | eqid 2622 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
10 | 9 | lpss 20946 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((limPt‘𝐽)‘𝑆) ⊆ ∪ 𝐽) |
11 | 4, 8, 10 | syl2anc 693 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) →
((limPt‘𝐽)‘𝑆) ⊆ ∪ 𝐽) |
12 | | simpl3 1066 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) |
13 | 11, 12 | sseldd 3604 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ ∪ 𝐽) |
14 | 13, 7 | eleqtrrd 2704 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ 𝑋) |
15 | | simpr 477 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → 𝑅 ∈
ℝ+) |
16 | 2 | blnei 22307 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃})) |
17 | 1, 14, 15, 16 | syl3anc 1326 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃})) |
18 | 9 | islp2 20949 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽
∧ 𝑃 ∈ ∪ 𝐽)
→ (𝑃 ∈
((limPt‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) |
19 | 4, 8, 13, 18 | syl3anc 1326 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) |
20 | 12, 19 | mpbid 222 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) →
∀𝑥 ∈
((nei‘𝐽)‘{𝑃})(𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) |
21 | | ineq1 3807 |
. . . . 5
⊢ (𝑥 = (𝑃(ball‘𝐷)𝑅) → (𝑥 ∩ (𝑆 ∖ {𝑃})) = ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃}))) |
22 | 21 | neeq1d 2853 |
. . . 4
⊢ (𝑥 = (𝑃(ball‘𝐷)𝑅) → ((𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅ ↔ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) |
23 | 22 | rspcva 3307 |
. . 3
⊢ (((𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃}) ∧ ∀𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) ≠ ∅) |
24 | 17, 20, 23 | syl2anc 693 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) ≠ ∅) |
25 | | elin 3796 |
. . . . 5
⊢ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) ↔ (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑆 ∖ {𝑃}))) |
26 | | eldifi 3732 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑆 ∖ {𝑃}) → 𝑥 ∈ 𝑆) |
27 | 26 | anim2i 593 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ 𝑆)) |
28 | 27 | ancomd 467 |
. . . . 5
⊢ ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅))) |
29 | 25, 28 | sylbi 207 |
. . . 4
⊢ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) → (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅))) |
30 | 29 | eximi 1762 |
. . 3
⊢
(∃𝑥 𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) → ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅))) |
31 | | n0 3931 |
. . 3
⊢ (((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃}))) |
32 | | df-rex 2918 |
. . 3
⊢
(∃𝑥 ∈
𝑆 𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅))) |
33 | 30, 31, 32 | 3imtr4i 281 |
. 2
⊢ (((𝑃(ball‘𝐷)𝑅) ∩ (𝑆 ∖ {𝑃})) ≠ ∅ → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) |
34 | 24, 33 | syl 17 |
1
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) →
∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) |