Theorem nlpineqsn

Description: For every point p of a subset A of X with no limit points, there exists an open set n that intersects A only at p . (Contributed by ML, 23-Mar-2021)

	Ref	Expression
Hypothesis	nlpineqsn.x	⊢ 𝑋 = ∪ 𝐽
Assertion	nlpineqsn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )

Proof

Step	Hyp	Ref	Expression
1		nlpineqsn.x	⊢ 𝑋 = ∪ 𝐽
2		simp1	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → 𝐽 ∈ Top )
3		simp2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → 𝐴 ⊆ 𝑋 )
4		ssel2	⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝑋 )
5	4	3adant1	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝑋 )
6	2 3 5	3jca	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑋 ) )
7		noel	⊢ ¬ 𝑝 ∈ ∅
8		eleq2	⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ → ( 𝑝 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑝 ∈ ∅ ) )
9	7 8	mtbiri	⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ → ¬ 𝑝 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) )
10	9	adantl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ¬ 𝑝 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) )
11	1	islp3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑝 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) ) )
12	11	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ( 𝑝 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) ) )
13	10 12	mtbid	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ¬ ∀ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) )
14		nne	⊢ ( ¬ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ↔ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ )
15	14	anbi2i	⊢ ( ( 𝑝 ∈ 𝑛 ∧ ¬ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) ↔ ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) )
16		annim	⊢ ( ( 𝑝 ∈ 𝑛 ∧ ¬ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) ↔ ¬ ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) )
17	15 16	bitr3i	⊢ ( ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ¬ ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) )
18	17	rexbii	⊢ ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ¬ ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) )
19		rexnal	⊢ ( ∃ 𝑛 ∈ 𝐽 ¬ ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) ↔ ¬ ∀ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) )
20	18 19	bitri	⊢ ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ¬ ∀ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 → ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) ≠ ∅ ) )
21	13 20	sylibr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) )
22	6 21	sylan	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) )
23		indif2	⊢ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ( ( 𝑛 ∩ 𝐴 ) ∖ { 𝑝 } )
24	23	eqeq1i	⊢ ( ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ↔ ( ( 𝑛 ∩ 𝐴 ) ∖ { 𝑝 } ) = ∅ )
25		ssdif0	⊢ ( ( 𝑛 ∩ 𝐴 ) ⊆ { 𝑝 } ↔ ( ( 𝑛 ∩ 𝐴 ) ∖ { 𝑝 } ) = ∅ )
26	24 25	bitr4i	⊢ ( ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ↔ ( 𝑛 ∩ 𝐴 ) ⊆ { 𝑝 } )
27		elin	⊢ ( 𝑝 ∈ ( 𝑛 ∩ 𝐴 ) ↔ ( 𝑝 ∈ 𝑛 ∧ 𝑝 ∈ 𝐴 ) )
28		sssn	⊢ ( ( 𝑛 ∩ 𝐴 ) ⊆ { 𝑝 } ↔ ( ( 𝑛 ∩ 𝐴 ) = ∅ ∨ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
29		n0i	⊢ ( 𝑝 ∈ ( 𝑛 ∩ 𝐴 ) → ¬ ( 𝑛 ∩ 𝐴 ) = ∅ )
30		biorf	⊢ ( ¬ ( 𝑛 ∩ 𝐴 ) = ∅ → ( ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ↔ ( ( 𝑛 ∩ 𝐴 ) = ∅ ∨ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) ) )
31	29 30	syl	⊢ ( 𝑝 ∈ ( 𝑛 ∩ 𝐴 ) → ( ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ↔ ( ( 𝑛 ∩ 𝐴 ) = ∅ ∨ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) ) )
32	28 31	bitr4id	⊢ ( 𝑝 ∈ ( 𝑛 ∩ 𝐴 ) → ( ( 𝑛 ∩ 𝐴 ) ⊆ { 𝑝 } ↔ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
33	27 32	sylbir	⊢ ( ( 𝑝 ∈ 𝑛 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑛 ∩ 𝐴 ) ⊆ { 𝑝 } ↔ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
34	26 33	syl5bb	⊢ ( ( 𝑝 ∈ 𝑛 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ↔ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
35	34	ancoms	⊢ ( ( 𝑝 ∈ 𝐴 ∧ 𝑝 ∈ 𝑛 ) → ( ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ↔ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
36	35	pm5.32da	⊢ ( 𝑝 ∈ 𝐴 → ( ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) ) )
37	36	rexbidv	⊢ ( 𝑝 ∈ 𝐴 → ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) ) )
38	37	3ad2ant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) ) )
39	38	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ ( 𝐴 ∖ { 𝑝 } ) ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) ) )
40	22 39	mpbid	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
41	40	3an1rs	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )
42	41	ralrimiva	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) = ∅ ) → ∀ 𝑝 ∈ 𝐴 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝐴 ) = { 𝑝 } ) )