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 ‘ 𝐷 ) 𝑅 ) )