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 β€˜ 𝐷 ) 𝑅 ) )