This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lpbl

Description: Every ball around a limit point P of a subset S includes a member of S (even if P e/ S ). (Contributed by NM, 9-Nov-2007) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypothesis mopni.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion lpbl ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 ineq1 ⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) = ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
3 2 neeq1d ⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → ( ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ↔ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
4 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )
5 simpl1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
6 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
7 5 6 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝐽 ∈ Top )
8 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑆 ⊆ 𝑋 )
9 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
10 5 9 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑋 = ∪ 𝐽 )
11 8 10 sseqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑆 ⊆ ∪ 𝐽 )
12 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
13 12 lpss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
14 7 11 13 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
15 14 4 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ∪ 𝐽 )
16 12 islp2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝑃 ∈ ∪ 𝐽 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
17 7 11 15 16 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
18 4 17 mpbid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑥 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
19 15 10 eleqtrrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ 𝑋 )
20 simpr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℝ+ )
21 1 blnei ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
22 5 19 20 21 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
23 3 18 22 rspcdva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
24 elin ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) )
25 eldifi ⊢ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) → 𝑥 ∈ 𝑆 )
26 25 anim2i ⊢ ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ 𝑆 ) )
27 26 ancomd ⊢ ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) )
28 24 27 sylbi ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) )
29 28 eximi ⊢ ( ∃ 𝑥 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) )
30 n0 ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
31 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) )
32 29 30 31 3imtr4i ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ → ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )
33 23 32 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )