Metamath Proof Explorer

Theorem nlpfvineqsn

Description: Given a subset A of X with no limit points, there exists a function from each point p of A to an open set intersecting A only at p . This proof uses the axiom of choice. (Contributed by ML, 23-Mar-2021) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 nlpineqsn.x 
 |-  X = U. J
2 simpl 
 |-  ( ( A e. V /\ ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) ) -> A e. V )
3 simp1 
 |-  ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> J e. Top )
4 3 elexd 
 |-  ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> J e. _V )
5 4 adantl 
 |-  ( ( A e. V /\ ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) ) -> J e. _V )
6 1 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 } ) )
7 simpr 
 |-  ( ( p e. n /\ ( n i^i A ) = { p } ) -> ( n i^i A ) = { p } )
8 7 reximi 
 |-  ( E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) -> E. n e. J ( n i^i A ) = { p } )
9 8 ralimi 
 |-  ( A. p e. A E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) -> A. p e. A E. n e. J ( n i^i A ) = { p } )
10 6 9 syl 
 |-  ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> A. p e. A E. n e. J ( n i^i A ) = { p } )
11 10 adantl 
 |-  ( ( A e. V /\ ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) ) -> A. p e. A E. n e. J ( n i^i A ) = { p } )
12 ineq1 
 |-  ( n = ( f ` p ) -> ( n i^i A ) = ( ( f ` p ) i^i A ) )
13 12 eqeq1d 
 |-  ( n = ( f ` p ) -> ( ( n i^i A ) = { p } <-> ( ( f ` p ) i^i A ) = { p } ) )
14 13 ac6 
 |-  ( ( A e. V /\ J e. _V /\ A. p e. A E. n e. J ( n i^i A ) = { p } ) -> E. f ( f : A --> J /\ A. p e. A ( ( f ` p ) i^i A ) = { p } ) )
15 2 5 11 14 syl3anc 
 |-  ( ( A e. V /\ ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) ) -> E. f ( f : A --> J /\ A. p e. A ( ( f ` p ) i^i A ) = { p } ) )
16 15 ex 
 |-  ( A e. V -> ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> E. f ( f : A --> J /\ A. p e. A ( ( f ` p ) i^i A ) = { p } ) ) )