Metamath Proof Explorer

Theorem nlpineqsn

Description: For every point p of a subset A of X with no limit points, there exists an open set n that intersects A only at p . (Contributed by ML, 23-Mar-2021)

Ref Expression
Hypothesis nlpineqsn.x 
|- X = U. J
Assertion nlpineqsn 
|- ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> A. p e. A E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) )

Proof

Step Hyp Ref Expression
1 nlpineqsn.x 
 |-  X = U. J
2 simp1 
 |-  ( ( J e. Top /\ A C_ X /\ p e. A ) -> J e. Top )
3 simp2 
 |-  ( ( J e. Top /\ A C_ X /\ p e. A ) -> A C_ X )
4 ssel2 
 |-  ( ( A C_ X /\ p e. A ) -> p e. X )
5 4 3adant1 
 |-  ( ( J e. Top /\ A C_ X /\ p e. A ) -> p e. X )
6 2 3 5 3jca 
 |-  ( ( J e. Top /\ A C_ X /\ p e. A ) -> ( J e. Top /\ A C_ X /\ p e. X ) )
7 noel 
 |-  -. p e. (/)
8 eleq2 
 |-  ( ( ( limPt ` J ) ` A ) = (/) -> ( p e. ( ( limPt ` J ) ` A ) <-> p e. (/) ) )
9 7 8 mtbiri 
 |-  ( ( ( limPt ` J ) ` A ) = (/) -> -. p e. ( ( limPt ` J ) ` A ) )
10 9 adantl 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. X ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> -. p e. ( ( limPt ` J ) ` A ) )
11 1 islp3 
 |-  ( ( J e. Top /\ A C_ X /\ p e. X ) -> ( p e. ( ( limPt ` J ) ` A ) <-> A. n e. J ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) ) )
12 11 adantr 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. X ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> ( p e. ( ( limPt ` J ) ` A ) <-> A. n e. J ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) ) )
13 10 12 mtbid 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. X ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> -. A. n e. J ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) )
14 nne 
 |-  ( -. ( n i^i ( A \ { p } ) ) =/= (/) <-> ( n i^i ( A \ { p } ) ) = (/) )
15 14 anbi2i 
 |-  ( ( p e. n /\ -. ( n i^i ( A \ { p } ) ) =/= (/) ) <-> ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) )
16 annim 
 |-  ( ( p e. n /\ -. ( n i^i ( A \ { p } ) ) =/= (/) ) <-> -. ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) )
17 15 16 bitr3i 
 |-  ( ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> -. ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) )
18 17 rexbii 
 |-  ( E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> E. n e. J -. ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) )
19 rexnal 
 |-  ( E. n e. J -. ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) <-> -. A. n e. J ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) )
20 18 19 bitri 
 |-  ( E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> -. A. n e. J ( p e. n -> ( n i^i ( A \ { p } ) ) =/= (/) ) )
21 13 20 sylibr 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. X ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) )
22 6 21 sylan 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. A ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) )
23 indif2 
 |-  ( n i^i ( A \ { p } ) ) = ( ( n i^i A ) \ { p } )
24 23 eqeq1i 
 |-  ( ( n i^i ( A \ { p } ) ) = (/) <-> ( ( n i^i A ) \ { p } ) = (/) )
25 ssdif0 
 |-  ( ( n i^i A ) C_ { p } <-> ( ( n i^i A ) \ { p } ) = (/) )
26 24 25 bitr4i 
 |-  ( ( n i^i ( A \ { p } ) ) = (/) <-> ( n i^i A ) C_ { p } )
27 elin 
 |-  ( p e. ( n i^i A ) <-> ( p e. n /\ p e. A ) )
28 sssn 
 |-  ( ( n i^i A ) C_ { p } <-> ( ( n i^i A ) = (/) \/ ( n i^i A ) = { p } ) )
29 n0i 
 |-  ( p e. ( n i^i A ) -> -. ( n i^i A ) = (/) )
30 biorf 
 |-  ( -. ( n i^i A ) = (/) -> ( ( n i^i A ) = { p } <-> ( ( n i^i A ) = (/) \/ ( n i^i A ) = { p } ) ) )
31 29 30 syl 
 |-  ( p e. ( n i^i A ) -> ( ( n i^i A ) = { p } <-> ( ( n i^i A ) = (/) \/ ( n i^i A ) = { p } ) ) )
32 28 31 bitr4id 
 |-  ( p e. ( n i^i A ) -> ( ( n i^i A ) C_ { p } <-> ( n i^i A ) = { p } ) )
33 27 32 sylbir 
 |-  ( ( p e. n /\ p e. A ) -> ( ( n i^i A ) C_ { p } <-> ( n i^i A ) = { p } ) )
34 26 33 bitrid 
 |-  ( ( p e. n /\ p e. A ) -> ( ( n i^i ( A \ { p } ) ) = (/) <-> ( n i^i A ) = { p } ) )
35 34 ancoms 
 |-  ( ( p e. A /\ p e. n ) -> ( ( n i^i ( A \ { p } ) ) = (/) <-> ( n i^i A ) = { p } ) )
36 35 pm5.32da 
 |-  ( p e. A -> ( ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> ( p e. n /\ ( n i^i A ) = { p } ) ) )
37 36 rexbidv 
 |-  ( p e. A -> ( E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) ) )
38 37 3ad2ant3 
 |-  ( ( J e. Top /\ A C_ X /\ p e. A ) -> ( E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) ) )
39 38 adantr 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. A ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> ( E. n e. J ( p e. n /\ ( n i^i ( A \ { p } ) ) = (/) ) <-> E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) ) )
40 22 39 mpbid 
 |-  ( ( ( J e. Top /\ A C_ X /\ p e. A ) /\ ( ( limPt ` J ) ` A ) = (/) ) -> E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) )
41 40 3an1rs 
 |-  ( ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) /\ p e. A ) -> E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) )
42 41 ralrimiva 
 |-  ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> A. p e. A E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) )