Metamath Proof Explorer

Theorem clsndisj

Description: Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 26-Feb-2007)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	clsndisj	$⊢ ((J \in Top \land S \subseteq X \land P \in cls (J) (S)) \land (U \in J \land P \in U)) \to U \cap S \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		simp1	$⊢ (J \in Top \land S \subseteq X \land P \in cls (J) (S)) \to J \in Top$
3		simp2	$⊢ (J \in Top \land S \subseteq X \land P \in cls (J) (S)) \to S \subseteq X$
4	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
5	4	sseld	$⊢ (J \in Top \land S \subseteq X) \to (P \in cls (J) (S) \to P \in X)$
6	5	3impia	$⊢ (J \in Top \land S \subseteq X \land P \in cls (J) (S)) \to P \in X$
7		simp3	$⊢ (J \in Top \land S \subseteq X \land P \in cls (J) (S)) \to P \in cls (J) (S)$
8	1	elcls	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in cls (J) (S) \leftrightarrow \forall x \in J (P \in x \to x \cap S \neq \emptyset))$
9	8	biimpa	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land P \in cls (J) (S)) \to \forall x \in J (P \in x \to x \cap S \neq \emptyset)$
10	2 3 6 7 9	syl31anc	$⊢ (J \in Top \land S \subseteq X \land P \in cls (J) (S)) \to \forall x \in J (P \in x \to x \cap S \neq \emptyset)$
11		eleq2	$⊢ x = U \to (P \in x \leftrightarrow P \in U)$
12		ineq1	$⊢ x = U \to x \cap S = U \cap S$
13	12	neeq1d	$⊢ x = U \to (x \cap S \neq \emptyset \leftrightarrow U \cap S \neq \emptyset)$
14	11 13	imbi12d	$⊢ x = U \to ((P \in x \to x \cap S \neq \emptyset) \leftrightarrow (P \in U \to U \cap S \neq \emptyset))$
15	14	rspccv	$⊢ \forall x \in J (P \in x \to x \cap S \neq \emptyset) \to (U \in J \to (P \in U \to U \cap S \neq \emptyset))$
16	15	imp32	$⊢ (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \land (U \in J \land P \in U)) \to U \cap S \neq \emptyset$
17	10 16	sylan	$⊢ ((J \in Top \land S \subseteq X \land P \in cls (J) (S)) \land (U \in J \land P \in U)) \to U \cap S \neq \emptyset$