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 | |
|
Assertion | nlpfvineqsn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nlpineqsn.x | |
|
2 | 1 | nlpineqsn | |
3 | simpr | |
|
4 | 3 | reximi | |
5 | 4 | ralimi | |
6 | 2 5 | syl | |
7 | ineq1 | |
|
8 | 7 | eqeq1d | |
9 | 8 | ac6sg | |
10 | 6 9 | syl5 | |