elcls

Description: Membership in a closure. Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 22-Feb-2007)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	cmclsopn	$⊢ (J \in Top \land S \subseteq X) \to X ∖ cls (J) (S) \in J$
3	2	3adant3	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to X ∖ cls (J) (S) \in J$
4	3	adantr	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \neg P \in cls (J) (S)) \to X ∖ cls (J) (S) \in J$
5		eldif	$⊢ P \in (X ∖ cls (J) (S)) \leftrightarrow (P \in X \land \neg P \in cls (J) (S))$
6	5	biimpri	$⊢ (P \in X \land \neg P \in cls (J) (S)) \to P \in (X ∖ cls (J) (S))$
7	6	3ad2antl3	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \neg P \in cls (J) (S)) \to P \in (X ∖ cls (J) (S))$
8		simpr	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq X$
9	1	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$
10	8 9	ssind	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq X \cap cls (J) (S)$
11		dfin4	$⊢ X \cap cls (J) (S) = X ∖ (X ∖ cls (J) (S))$
12	10 11	sseqtrdi	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq X ∖ (X ∖ cls (J) (S))$
13		reldisj	$⊢ S \subseteq X \to (S \cap (X ∖ cls (J) (S)) = \emptyset \leftrightarrow S \subseteq X ∖ (X ∖ cls (J) (S)))$
14	13	adantl	$⊢ (J \in Top \land S \subseteq X) \to (S \cap (X ∖ cls (J) (S)) = \emptyset \leftrightarrow S \subseteq X ∖ (X ∖ cls (J) (S)))$
15	12 14	mpbird	$⊢ (J \in Top \land S \subseteq X) \to S \cap (X ∖ cls (J) (S)) = \emptyset$
16		nne	$⊢ \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset \leftrightarrow (X ∖ cls (J) (S)) \cap S = \emptyset$
17		incom	$⊢ (X ∖ cls (J) (S)) \cap S = S \cap (X ∖ cls (J) (S))$
18	17	eqeq1i	$⊢ (X ∖ cls (J) (S)) \cap S = \emptyset \leftrightarrow S \cap (X ∖ cls (J) (S)) = \emptyset$
19	16 18	bitri	$⊢ \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset \leftrightarrow S \cap (X ∖ cls (J) (S)) = \emptyset$
20	15 19	sylibr	$⊢ (J \in Top \land S \subseteq X) \to \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset$
21	20	3adant3	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset$
22	21	adantr	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \neg P \in cls (J) (S)) \to \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset$
23		eleq2	$⊢ x = X ∖ cls (J) (S) \to (P \in x \leftrightarrow P \in (X ∖ cls (J) (S)))$
24		ineq1	$⊢ x = X ∖ cls (J) (S) \to x \cap S = (X ∖ cls (J) (S)) \cap S$
25	24	neeq1d	$⊢ x = X ∖ cls (J) (S) \to (x \cap S \neq \emptyset \leftrightarrow (X ∖ cls (J) (S)) \cap S \neq \emptyset)$
26	25	notbid	$⊢ x = X ∖ cls (J) (S) \to (\neg x \cap S \neq \emptyset \leftrightarrow \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset)$
27	23 26	anbi12d	$⊢ x = X ∖ cls (J) (S) \to ((P \in x \land \neg x \cap S \neq \emptyset) \leftrightarrow (P \in (X ∖ cls (J) (S)) \land \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset))$
28	27	rspcev	$⊢ (X ∖ cls (J) (S) \in J \land (P \in (X ∖ cls (J) (S)) \land \neg (X ∖ cls (J) (S)) \cap S \neq \emptyset)) \to \exists x \in J (P \in x \land \neg x \cap S \neq \emptyset)$
29	4 7 22 28	syl12anc	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \neg P \in cls (J) (S)) \to \exists x \in J (P \in x \land \neg x \cap S \neq \emptyset)$
30		incom	$⊢ S \cap x = x \cap S$
31	30	eqeq1i	$⊢ S \cap x = \emptyset \leftrightarrow x \cap S = \emptyset$
32		df-ne	$⊢ x \cap S \neq \emptyset \leftrightarrow \neg x \cap S = \emptyset$
33	32	con2bii	$⊢ x \cap S = \emptyset \leftrightarrow \neg x \cap S \neq \emptyset$
34	31 33	bitri	$⊢ S \cap x = \emptyset \leftrightarrow \neg x \cap S \neq \emptyset$
35	1	opncld	$⊢ (J \in Top \land x \in J) \to X ∖ x \in Clsd (J)$
36	35	adantlr	$⊢ ((J \in Top \land S \subseteq X) \land x \in J) \to X ∖ x \in Clsd (J)$
37		reldisj	$⊢ S \subseteq X \to (S \cap x = \emptyset \leftrightarrow S \subseteq X ∖ x)$
38	37	biimpa	$⊢ (S \subseteq X \land S \cap x = \emptyset) \to S \subseteq X ∖ x$
39	38	ad4ant24	$⊢ (((J \in Top \land S \subseteq X) \land x \in J) \land S \cap x = \emptyset) \to S \subseteq X ∖ x$
40	1	clsss2	$⊢ (X ∖ x \in Clsd (J) \land S \subseteq X ∖ x) \to cls (J) (S) \subseteq X ∖ x$
41	36 39 40	syl2an2r	$⊢ (((J \in Top \land S \subseteq X) \land x \in J) \land S \cap x = \emptyset) \to cls (J) (S) \subseteq X ∖ x$
42	41	sseld	$⊢ (((J \in Top \land S \subseteq X) \land x \in J) \land S \cap x = \emptyset) \to (P \in cls (J) (S) \to P \in (X ∖ x))$
43		eldifn	$⊢ P \in (X ∖ x) \to \neg P \in x$
44	42 43	syl6	$⊢ (((J \in Top \land S \subseteq X) \land x \in J) \land S \cap x = \emptyset) \to (P \in cls (J) (S) \to \neg P \in x)$
45	44	con2d	$⊢ (((J \in Top \land S \subseteq X) \land x \in J) \land S \cap x = \emptyset) \to (P \in x \to \neg P \in cls (J) (S))$
46	34 45	sylan2br	$⊢ (((J \in Top \land S \subseteq X) \land x \in J) \land \neg x \cap S \neq \emptyset) \to (P \in x \to \neg P \in cls (J) (S))$
47	46	exp31	$⊢ (J \in Top \land S \subseteq X) \to (x \in J \to (\neg x \cap S \neq \emptyset \to (P \in x \to \neg P \in cls (J) (S))))$
48	47	com34	$⊢ (J \in Top \land S \subseteq X) \to (x \in J \to (P \in x \to (\neg x \cap S \neq \emptyset \to \neg P \in cls (J) (S))))$
49	48	imp4a	$⊢ (J \in Top \land S \subseteq X) \to (x \in J \to ((P \in x \land \neg x \cap S \neq \emptyset) \to \neg P \in cls (J) (S)))$
50	49	rexlimdv	$⊢ (J \in Top \land S \subseteq X) \to (\exists x \in J (P \in x \land \neg x \cap S \neq \emptyset) \to \neg P \in cls (J) (S))$
51	50	imp	$⊢ ((J \in Top \land S \subseteq X) \land \exists x \in J (P \in x \land \neg x \cap S \neq \emptyset)) \to \neg P \in cls (J) (S)$
52	51	3adantl3	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \exists x \in J (P \in x \land \neg x \cap S \neq \emptyset)) \to \neg P \in cls (J) (S)$
53	29 52	impbida	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (\neg P \in cls (J) (S) \leftrightarrow \exists x \in J (P \in x \land \neg x \cap S \neq \emptyset))$
54		rexanali	$⊢ \exists x \in J (P \in x \land \neg x \cap S \neq \emptyset) \leftrightarrow \neg \forall x \in J (P \in x \to x \cap S \neq \emptyset)$
55	53 54	bitrdi	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (\neg P \in cls (J) (S) \leftrightarrow \neg \forall x \in J (P \in x \to x \cap S \neq \emptyset))$
56	55	con4bid	$⊢ (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))$

Metamath Proof Explorer

Theorem elcls

Proof