neindisj

Description: Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

		Ref	Expression
	Hypothesis	neips.1	$⊢ X = ⋃ J$
	Assertion	neindisj	$⊢ ((J \in Top \land S \subseteq X) \land (P \in cls (J) (S) \land N \in nei (J) (\{P\}))) \to N \cap S \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		neips.1	$⊢ X = ⋃ J$
2	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
3	2	sseld	$⊢ (J \in Top \land S \subseteq X) \to (P \in cls (J) (S) \to P \in X)$
4	3	impr	$⊢ (J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \to P \in X$
5	1	isneip	$⊢ (J \in Top \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)))$
6	4 5	syldan	$⊢ (J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)))$
7		3anass	$⊢ (J \in Top \land S \subseteq X \land P \in cls (J) (S)) \leftrightarrow (J \in Top \land (S \subseteq X \land P \in cls (J) (S)))$
8	1	clsndisj	$⊢ ((J \in Top \land S \subseteq X \land P \in cls (J) (S)) \land (g \in J \land P \in g)) \to g \cap S \neq \emptyset$
9	7 8	sylanbr	$⊢ ((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land (g \in J \land P \in g)) \to g \cap S \neq \emptyset$
10	9	anassrs	$⊢ (((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land g \in J) \land P \in g) \to g \cap S \neq \emptyset$
11	10	adantllr	$⊢ ((((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land N \subseteq X) \land g \in J) \land P \in g) \to g \cap S \neq \emptyset$
12	11	adantrr	$⊢ ((((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land N \subseteq X) \land g \in J) \land (P \in g \land g \subseteq N)) \to g \cap S \neq \emptyset$
13		ssdisj	$⊢ (g \subseteq N \land N \cap S = \emptyset) \to g \cap S = \emptyset$
14	13	ex	$⊢ g \subseteq N \to (N \cap S = \emptyset \to g \cap S = \emptyset)$
15	14	necon3d	$⊢ g \subseteq N \to (g \cap S \neq \emptyset \to N \cap S \neq \emptyset)$
16	15	ad2antll	$⊢ ((((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land N \subseteq X) \land g \in J) \land (P \in g \land g \subseteq N)) \to (g \cap S \neq \emptyset \to N \cap S \neq \emptyset)$
17	12 16	mpd	$⊢ ((((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land N \subseteq X) \land g \in J) \land (P \in g \land g \subseteq N)) \to N \cap S \neq \emptyset$
18	17	rexlimdva2	$⊢ ((J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \land N \subseteq X) \to (\exists g \in J (P \in g \land g \subseteq N) \to N \cap S \neq \emptyset)$
19	18	expimpd	$⊢ (J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \to ((N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)) \to N \cap S \neq \emptyset)$
20	6 19	sylbid	$⊢ (J \in Top \land (S \subseteq X \land P \in cls (J) (S))) \to (N \in nei (J) (\{P\}) \to N \cap S \neq \emptyset)$
21	20	exp32	$⊢ J \in Top \to (S \subseteq X \to (P \in cls (J) (S) \to (N \in nei (J) (\{P\}) \to N \cap S \neq \emptyset)))$
22	21	imp43	$⊢ ((J \in Top \land S \subseteq X) \land (P \in cls (J) (S) \land N \in nei (J) (\{P\}))) \to N \cap S \neq \emptyset$

Metamath Proof Explorer

Theorem neindisj

Proof