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	$⊢ A \in V \to ((J \in Top \land A \subseteq X \land limPt (J) (A) = \emptyset) \to \exists f (f : A ⟶ J \land \forall p \in A f (p) \cap A = \{p\}))$

Proof

Step	Hyp	Ref	Expression
1		nlpineqsn.x	$⊢ X = ⋃ J$
2	1	nlpineqsn	$⊢ (J \in Top \land A \subseteq X \land limPt (J) (A) = \emptyset) \to \forall p \in A \exists n \in J (p \in n \land n \cap A = \{p\})$
3		simpr	$⊢ (p \in n \land n \cap A = \{p\}) \to n \cap A = \{p\}$
4	3	reximi	$⊢ \exists n \in J (p \in n \land n \cap A = \{p\}) \to \exists n \in J n \cap A = \{p\}$
5	4	ralimi	$⊢ \forall p \in A \exists n \in J (p \in n \land n \cap A = \{p\}) \to \forall p \in A \exists n \in J n \cap A = \{p\}$
6	2 5	syl	$⊢ (J \in Top \land A \subseteq X \land limPt (J) (A) = \emptyset) \to \forall p \in A \exists n \in J n \cap A = \{p\}$
7		ineq1	$⊢ n = f (p) \to n \cap A = f (p) \cap A$
8	7	eqeq1d	$⊢ n = f (p) \to (n \cap A = \{p\} \leftrightarrow f (p) \cap A = \{p\})$
9	8	ac6sg	$⊢ A \in V \to (\forall p \in A \exists n \in J n \cap A = \{p\} \to \exists f (f : A ⟶ J \land \forall p \in A f (p) \cap A = \{p\}))$
10	6 9	syl5	$⊢ A \in V \to ((J \in Top \land A \subseteq X \land limPt (J) (A) = \emptyset) \to \exists f (f : A ⟶ J \land \forall p \in A f (p) \cap A = \{p\}))$