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)

Ref Expression
Hypothesis nlpineqsn.x X=J
Assertion nlpfvineqsn AVJTopAXlimPtJA=ff:AJpAfpA=p

Proof

Step Hyp Ref Expression
1 nlpineqsn.x X=J
2 1 nlpineqsn JTopAXlimPtJA=pAnJpnnA=p
3 simpr pnnA=pnA=p
4 3 reximi nJpnnA=pnJnA=p
5 4 ralimi pAnJpnnA=ppAnJnA=p
6 2 5 syl JTopAXlimPtJA=pAnJnA=p
7 ineq1 n=fpnA=fpA
8 7 eqeq1d n=fpnA=pfpA=p
9 8 ac6sg AVpAnJnA=pff:AJpAfpA=p
10 6 9 syl5 AVJTopAXlimPtJA=ff:AJpAfpA=p