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	⊢ 𝑋 = ∪ 𝐽
Assertion	nlpfvineqsn	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		nlpineqsn.x	⊢ 𝑋 = ∪ 𝐽
2		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) ) → 𝐴 ∈ 𝑉 )
3		simp1	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → 𝐽 ∈ Top )
4	3	elexd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → 𝐽 ∈ V )
5	4	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) ) → 𝐽 ∈ V )
6	1	nlpineqsn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
7		simpr	⊢ ( ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
8	7	reximi	⊢ ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
9	8	ralimi	⊢ ( ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
10	6 9	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
11	10	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
12		ineq1	⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( 𝑛 ∩ 𝐴 ) = ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) )
13	12	eqeq1d	⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ↔ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
14	13	ac6	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ V ∧ ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
15	2 5 11 14	syl3anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
16	15	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ) )