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	$⊢ X = ⋃ J$
	Assertion	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\})$

Proof

Step	Hyp	Ref	Expression
1		nlpineqsn.x	$⊢ X = ⋃ J$
2		simp1	$⊢ (J \in Top \land A \subseteq X \land p \in A) \to J \in Top$
3		simp2	$⊢ (J \in Top \land A \subseteq X \land p \in A) \to A \subseteq X$
4		ssel2	$⊢ (A \subseteq X \land p \in A) \to p \in X$
5	4	3adant1	$⊢ (J \in Top \land A \subseteq X \land p \in A) \to p \in X$
6	2 3 5	3jca	$⊢ (J \in Top \land A \subseteq X \land p \in A) \to (J \in Top \land A \subseteq X \land p \in X)$
7		noel	$⊢ \neg p \in \emptyset$
8		eleq2	$⊢ limPt (J) (A) = \emptyset \to (p \in limPt (J) (A) \leftrightarrow p \in \emptyset)$
9	7 8	mtbiri	$⊢ limPt (J) (A) = \emptyset \to \neg p \in limPt (J) (A)$
10	9	adantl	$⊢ ((J \in Top \land A \subseteq X \land p \in X) \land limPt (J) (A) = \emptyset) \to \neg p \in limPt (J) (A)$
11	1	islp3	$⊢ (J \in Top \land A \subseteq X \land p \in X) \to (p \in limPt (J) (A) \leftrightarrow \forall n \in J (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset))$
12	11	adantr	$⊢ ((J \in Top \land A \subseteq X \land p \in X) \land limPt (J) (A) = \emptyset) \to (p \in limPt (J) (A) \leftrightarrow \forall n \in J (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset))$
13	10 12	mtbid	$⊢ ((J \in Top \land A \subseteq X \land p \in X) \land limPt (J) (A) = \emptyset) \to \neg \forall n \in J (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset)$
14		nne	$⊢ \neg n \cap (A ∖ \{p\}) \neq \emptyset \leftrightarrow n \cap (A ∖ \{p\}) = \emptyset$
15	14	anbi2i	$⊢ (p \in n \land \neg n \cap (A ∖ \{p\}) \neq \emptyset) \leftrightarrow (p \in n \land n \cap (A ∖ \{p\}) = \emptyset)$
16		annim	$⊢ (p \in n \land \neg n \cap (A ∖ \{p\}) \neq \emptyset) \leftrightarrow \neg (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset)$
17	15 16	bitr3i	$⊢ (p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow \neg (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset)$
18	17	rexbii	$⊢ \exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow \exists n \in J \neg (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset)$
19		rexnal	$⊢ \exists n \in J \neg (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset) \leftrightarrow \neg \forall n \in J (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset)$
20	18 19	bitri	$⊢ \exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow \neg \forall n \in J (p \in n \to n \cap (A ∖ \{p\}) \neq \emptyset)$
21	13 20	sylibr	$⊢ ((J \in Top \land A \subseteq X \land p \in X) \land limPt (J) (A) = \emptyset) \to \exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset)$
22	6 21	sylan	$⊢ ((J \in Top \land A \subseteq X \land p \in A) \land limPt (J) (A) = \emptyset) \to \exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset)$
23		indif2	$⊢ n \cap (A ∖ \{p\}) = (n \cap A) ∖ \{p\}$
24	23	eqeq1i	$⊢ n \cap (A ∖ \{p\}) = \emptyset \leftrightarrow (n \cap A) ∖ \{p\} = \emptyset$
25		ssdif0	$⊢ n \cap A \subseteq \{p\} \leftrightarrow (n \cap A) ∖ \{p\} = \emptyset$
26	24 25	bitr4i	$⊢ n \cap (A ∖ \{p\}) = \emptyset \leftrightarrow n \cap A \subseteq \{p\}$
27		elin	$⊢ p \in (n \cap A) \leftrightarrow (p \in n \land p \in A)$
28		n0i	$⊢ p \in (n \cap A) \to \neg n \cap A = \emptyset$
29		biorf	$⊢ \neg n \cap A = \emptyset \to (n \cap A = \{p\} \leftrightarrow (n \cap A = \emptyset \lor n \cap A = \{p\}))$
30	28 29	syl	$⊢ p \in (n \cap A) \to (n \cap A = \{p\} \leftrightarrow (n \cap A = \emptyset \lor n \cap A = \{p\}))$
31		sssn	$⊢ n \cap A \subseteq \{p\} \leftrightarrow (n \cap A = \emptyset \lor n \cap A = \{p\})$
32	30 31	syl6rbbr	$⊢ p \in (n \cap A) \to (n \cap A \subseteq \{p\} \leftrightarrow n \cap A = \{p\})$
33	27 32	sylbir	$⊢ (p \in n \land p \in A) \to (n \cap A \subseteq \{p\} \leftrightarrow n \cap A = \{p\})$
34	26 33	syl5bb	$⊢ (p \in n \land p \in A) \to (n \cap (A ∖ \{p\}) = \emptyset \leftrightarrow n \cap A = \{p\})$
35	34	ancoms	$⊢ (p \in A \land p \in n) \to (n \cap (A ∖ \{p\}) = \emptyset \leftrightarrow n \cap A = \{p\})$
36	35	pm5.32da	$⊢ p \in A \to ((p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow (p \in n \land n \cap A = \{p\}))$
37	36	rexbidv	$⊢ p \in A \to (\exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow \exists n \in J (p \in n \land n \cap A = \{p\}))$
38	37	3ad2ant3	$⊢ (J \in Top \land A \subseteq X \land p \in A) \to (\exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow \exists n \in J (p \in n \land n \cap A = \{p\}))$
39	38	adantr	$⊢ ((J \in Top \land A \subseteq X \land p \in A) \land limPt (J) (A) = \emptyset) \to (\exists n \in J (p \in n \land n \cap (A ∖ \{p\}) = \emptyset) \leftrightarrow \exists n \in J (p \in n \land n \cap A = \{p\}))$
40	22 39	mpbid	$⊢ ((J \in Top \land A \subseteq X \land p \in A) \land limPt (J) (A) = \emptyset) \to \exists n \in J (p \in n \land n \cap A = \{p\})$
41	40	3an1rs	$⊢ ((J \in Top \land A \subseteq X \land limPt (J) (A) = \emptyset) \land p \in A) \to \exists n \in J (p \in n \land n \cap A = \{p\})$
42	41	ralrimiva	$⊢ (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\})$

Metamath Proof Explorer

Theorem nlpineqsn

Proof