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)

	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	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 } ) )
3		simpr	|- ( ( p e. n /\ ( n i^i A ) = { p } ) -> ( n i^i A ) = { p } )
4	3	reximi	|- ( E. n e. J ( p e. n /\ ( n i^i A ) = { p } ) -> E. n e. J ( n i^i A ) = { p } )
5	4	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 } )
6	2 5	syl	|- ( ( J e. Top /\ A C_ X /\ ( ( limPt ` J ) ` A ) = (/) ) -> A. p e. A E. n e. J ( n i^i A ) = { p } )
7		ineq1	|- ( n = ( f ` p ) -> ( n i^i A ) = ( ( f ` p ) i^i A ) )
8	7	eqeq1d	|- ( n = ( f ` p ) -> ( ( n i^i A ) = { p } <-> ( ( f ` p ) i^i A ) = { p } ) )
9	8	ac6sg	|- ( A 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 } ) ) )
10	6 9	syl5	|- ( 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 } ) ) )