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 = ⋃ J
Assertion nlpfvineqsn ⊢ A ∈ V → J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → ∃ f f : A ⟶ J ∧ ∀ p ∈ A f ⁡ p ∩ A = p

Proof

Step Hyp Ref Expression
1 nlpineqsn.x ⊢ X = ⋃ J
2 simpl ⊢ A ∈ V ∧ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → A ∈ V
3 simp1 ⊢ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → J ∈ Top
4 3 elexd ⊢ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → J ∈ V
5 4 adantl ⊢ A ∈ V ∧ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → J ∈ V
6 1 nlpineqsn ⊢ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → ∀ p ∈ A ∃ n ∈ J p ∈ n ∧ n ∩ A = p
7 simpr ⊢ p ∈ n ∧ n ∩ A = p → n ∩ A = p
8 7 reximi ⊢ ∃ n ∈ J p ∈ n ∧ n ∩ A = p → ∃ n ∈ J n ∩ A = p
9 8 ralimi ⊢ ∀ p ∈ A ∃ n ∈ J p ∈ n ∧ n ∩ A = p → ∀ p ∈ A ∃ n ∈ J n ∩ A = p
10 6 9 syl ⊢ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → ∀ p ∈ A ∃ n ∈ J n ∩ A = p
11 10 adantl ⊢ A ∈ V ∧ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → ∀ p ∈ A ∃ n ∈ J n ∩ A = p
12 ineq1 ⊢ n = f ⁡ p → n ∩ A = f ⁡ p ∩ A
13 12 eqeq1d ⊢ n = f ⁡ p → n ∩ A = p ↔ f ⁡ p ∩ A = p
14 13 ac6 ⊢ A ∈ V ∧ J ∈ V ∧ ∀ p ∈ A ∃ n ∈ J n ∩ A = p → ∃ f f : A ⟶ J ∧ ∀ p ∈ A f ⁡ p ∩ A = p
15 2 5 11 14 syl3anc ⊢ A ∈ V ∧ J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → ∃ f f : A ⟶ J ∧ ∀ p ∈ A f ⁡ p ∩ A = p
16 15 ex ⊢ A ∈ V → J ∈ Top ∧ A ⊆ X ∧ limPt ⁡ J ⁡ A = ∅ → ∃ f f : A ⟶ J ∧ ∀ p ∈ A f ⁡ p ∩ A = p