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 
|- J = ( MetOpen ` D )
Assertion lpbl 
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> E. x e. S x e. ( P ( ball ` D ) R ) )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 ineq1 
 |-  ( x = ( P ( ball ` D ) R ) -> ( x i^i ( S \ { P } ) ) = ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) )
3 2 neeq1d 
 |-  ( x = ( P ( ball ` D ) R ) -> ( ( x i^i ( S \ { P } ) ) =/= (/) <-> ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) =/= (/) ) )
4 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> P e. ( ( limPt ` J ) ` S ) )
5 simpl1 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> D e. ( *Met ` X ) )
6 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
7 5 6 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> J e. Top )
8 simpl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> S C_ X )
9 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
10 5 9 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> X = U. J )
11 8 10 sseqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> S C_ U. J )
12 eqid 
 |-  U. J = U. J
13 12 lpss 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( limPt ` J ) ` S ) C_ U. J )
14 7 11 13 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> ( ( limPt ` J ) ` S ) C_ U. J )
15 14 4 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> P e. U. J )
16 12 islp2 
 |-  ( ( J e. Top /\ S C_ U. J /\ P e. U. J ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. x e. ( ( nei ` J ) ` { P } ) ( x i^i ( S \ { P } ) ) =/= (/) ) )
17 7 11 15 16 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. x e. ( ( nei ` J ) ` { P } ) ( x i^i ( S \ { P } ) ) =/= (/) ) )
18 4 17 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> A. x e. ( ( nei ` J ) ` { P } ) ( x i^i ( S \ { P } ) ) =/= (/) )
19 15 10 eleqtrrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> P e. X )
20 simpr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> R e. RR+ )
21 1 blnei 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )
22 5 19 20 21 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )
23 3 18 22 rspcdva 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) =/= (/) )
24 elin 
 |-  ( x e. ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) <-> ( x e. ( P ( ball ` D ) R ) /\ x e. ( S \ { P } ) ) )
25 eldifi 
 |-  ( x e. ( S \ { P } ) -> x e. S )
26 25 anim2i 
 |-  ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( S \ { P } ) ) -> ( x e. ( P ( ball ` D ) R ) /\ x e. S ) )
27 26 ancomd 
 |-  ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( S \ { P } ) ) -> ( x e. S /\ x e. ( P ( ball ` D ) R ) ) )
28 24 27 sylbi 
 |-  ( x e. ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) -> ( x e. S /\ x e. ( P ( ball ` D ) R ) ) )
29 28 eximi 
 |-  ( E. x x e. ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) -> E. x ( x e. S /\ x e. ( P ( ball ` D ) R ) ) )
30 n0 
 |-  ( ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) =/= (/) <-> E. x x e. ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) )
31 df-rex 
 |-  ( E. x e. S x e. ( P ( ball ` D ) R ) <-> E. x ( x e. S /\ x e. ( P ( ball ` D ) R ) ) )
32 29 30 31 3imtr4i 
 |-  ( ( ( P ( ball ` D ) R ) i^i ( S \ { P } ) ) =/= (/) -> E. x e. S x e. ( P ( ball ` D ) R ) )
33 23 32 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> E. x e. S x e. ( P ( ball ` D ) R ) )