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

Proof

Step	Hyp	Ref	Expression
1		nlpineqsn.x	⊢ 𝑋 = ∪ 𝐽
2	1	nlpineqsn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
3		simpr	⊢ ( ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
4	3	reximi	⊢ ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
5	4	ralimi	⊢ ( ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
6	2 5	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } )
7		ineq1	⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( 𝑛 ∩ 𝐴 ) = ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) )
8	7	eqeq1d	⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ↔ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
9	8	ac6sg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝐴 ) = { 𝑝 } → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ) )
10	6 9	syl5	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ) )