clsval2

Description: Express closure in terms of interior. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	clsval2	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = X ∖ int (J) (X ∖ S)$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		df-rab	$⊢ \{z \in Clsd (J) \| S \subseteq z\} = \{z \| (z \in Clsd (J) \land S \subseteq z)\}$
3	1	cldopn	$⊢ z \in Clsd (J) \to X ∖ z \in J$
4	3	ad2antrl	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to X ∖ z \in J$
5		sscon	$⊢ S \subseteq z \to X ∖ z \subseteq X ∖ S$
6	5	ad2antll	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to X ∖ z \subseteq X ∖ S$
7	1	topopn	$⊢ J \in Top \to X \in J$
8		difexg	$⊢ X \in J \to X ∖ z \in V$
9		elpwg	$⊢ X ∖ z \in V \to (X ∖ z \in 𝒫 (X ∖ S) \leftrightarrow X ∖ z \subseteq X ∖ S)$
10	7 8 9	3syl	$⊢ J \in Top \to (X ∖ z \in 𝒫 (X ∖ S) \leftrightarrow X ∖ z \subseteq X ∖ S)$
11	10	ad2antrr	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to (X ∖ z \in 𝒫 (X ∖ S) \leftrightarrow X ∖ z \subseteq X ∖ S)$
12	6 11	mpbird	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to X ∖ z \in 𝒫 (X ∖ S)$
13	4 12	elind	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to X ∖ z \in (J \cap 𝒫 (X ∖ S))$
14	1	cldss	$⊢ z \in Clsd (J) \to z \subseteq X$
15	14	ad2antrl	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to z \subseteq X$
16		dfss4	$⊢ z \subseteq X \leftrightarrow X ∖ (X ∖ z) = z$
17	15 16	sylib	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to X ∖ (X ∖ z) = z$
18	17	eqcomd	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to z = X ∖ (X ∖ z)$
19		difeq2	$⊢ x = X ∖ z \to X ∖ x = X ∖ (X ∖ z)$
20	19	rspceeqv	$⊢ (X ∖ z \in (J \cap 𝒫 (X ∖ S)) \land z = X ∖ (X ∖ z)) \to \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x$
21	13 18 20	syl2anc	$⊢ ((J \in Top \land S \subseteq X) \land (z \in Clsd (J) \land S \subseteq z)) \to \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x$
22	21	ex	$⊢ (J \in Top \land S \subseteq X) \to ((z \in Clsd (J) \land S \subseteq z) \to \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x)$
23		simpl	$⊢ (J \in Top \land S \subseteq X) \to J \in Top$
24		elinel1	$⊢ x \in (J \cap 𝒫 (X ∖ S)) \to x \in J$
25	1	opncld	$⊢ (J \in Top \land x \in J) \to X ∖ x \in Clsd (J)$
26	23 24 25	syl2an	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to X ∖ x \in Clsd (J)$
27		elinel2	$⊢ x \in (J \cap 𝒫 (X ∖ S)) \to x \in 𝒫 (X ∖ S)$
28	27	adantl	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to x \in 𝒫 (X ∖ S)$
29	28	elpwid	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to x \subseteq X ∖ S$
30	29	difss2d	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to x \subseteq X$
31		simplr	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to S \subseteq X$
32		ssconb	$⊢ (x \subseteq X \land S \subseteq X) \to (x \subseteq X ∖ S \leftrightarrow S \subseteq X ∖ x)$
33	30 31 32	syl2anc	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to (x \subseteq X ∖ S \leftrightarrow S \subseteq X ∖ x)$
34	29 33	mpbid	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to S \subseteq X ∖ x$
35	26 34	jca	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to (X ∖ x \in Clsd (J) \land S \subseteq X ∖ x)$
36		eleq1	$⊢ z = X ∖ x \to (z \in Clsd (J) \leftrightarrow X ∖ x \in Clsd (J))$
37		sseq2	$⊢ z = X ∖ x \to (S \subseteq z \leftrightarrow S \subseteq X ∖ x)$
38	36 37	anbi12d	$⊢ z = X ∖ x \to ((z \in Clsd (J) \land S \subseteq z) \leftrightarrow (X ∖ x \in Clsd (J) \land S \subseteq X ∖ x))$
39	35 38	syl5ibrcom	$⊢ ((J \in Top \land S \subseteq X) \land x \in (J \cap 𝒫 (X ∖ S))) \to (z = X ∖ x \to (z \in Clsd (J) \land S \subseteq z))$
40	39	rexlimdva	$⊢ (J \in Top \land S \subseteq X) \to (\exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x \to (z \in Clsd (J) \land S \subseteq z))$
41	22 40	impbid	$⊢ (J \in Top \land S \subseteq X) \to ((z \in Clsd (J) \land S \subseteq z) \leftrightarrow \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x)$
42	41	abbidv	$⊢ (J \in Top \land S \subseteq X) \to \{z \| (z \in Clsd (J) \land S \subseteq z)\} = \{z \| \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x\}$
43	2 42	syl5eq	$⊢ (J \in Top \land S \subseteq X) \to \{z \in Clsd (J) \| S \subseteq z\} = \{z \| \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x\}$
44	43	inteqd	$⊢ (J \in Top \land S \subseteq X) \to ⋂ \{z \in Clsd (J) \| S \subseteq z\} = ⋂ \{z \| \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x\}$
45		difexg	$⊢ X \in J \to X ∖ x \in V$
46	45	ralrimivw	$⊢ X \in J \to \forall x \in (J \cap 𝒫 (X ∖ S)) X ∖ x \in V$
47		dfiin2g	$⊢ \forall x \in (J \cap 𝒫 (X ∖ S)) X ∖ x \in V \to ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x) = ⋂ \{z \| \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x\}$
48	7 46 47	3syl	$⊢ J \in Top \to ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x) = ⋂ \{z \| \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x\}$
49	48	adantr	$⊢ (J \in Top \land S \subseteq X) \to ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x) = ⋂ \{z \| \exists x \in (J \cap 𝒫 (X ∖ S)) z = X ∖ x\}$
50	44 49	eqtr4d	$⊢ (J \in Top \land S \subseteq X) \to ⋂ \{z \in Clsd (J) \| S \subseteq z\} = ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x)$
51	1	clsval	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = ⋂ \{z \in Clsd (J) \| S \subseteq z\}$
52		uniiun	$⊢ ⋃ (J \cap 𝒫 (X ∖ S)) = ⋃_{x \in J \cap 𝒫 (X ∖ S)} x$
53	52	difeq2i	$⊢ X ∖ ⋃ (J \cap 𝒫 (X ∖ S)) = X ∖ ⋃_{x \in J \cap 𝒫 (X ∖ S)} x$
54	53	a1i	$⊢ (J \in Top \land S \subseteq X) \to X ∖ ⋃ (J \cap 𝒫 (X ∖ S)) = X ∖ ⋃_{x \in J \cap 𝒫 (X ∖ S)} x$
55		0opn	$⊢ J \in Top \to \emptyset \in J$
56	55	adantr	$⊢ (J \in Top \land S \subseteq X) \to \emptyset \in J$
57		0elpw	$⊢ \emptyset \in 𝒫 (X ∖ S)$
58	57	a1i	$⊢ (J \in Top \land S \subseteq X) \to \emptyset \in 𝒫 (X ∖ S)$
59	56 58	elind	$⊢ (J \in Top \land S \subseteq X) \to \emptyset \in (J \cap 𝒫 (X ∖ S))$
60		ne0i	$⊢ \emptyset \in (J \cap 𝒫 (X ∖ S)) \to J \cap 𝒫 (X ∖ S) \neq \emptyset$
61		iindif2	$⊢ J \cap 𝒫 (X ∖ S) \neq \emptyset \to ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x) = X ∖ ⋃_{x \in J \cap 𝒫 (X ∖ S)} x$
62	59 60 61	3syl	$⊢ (J \in Top \land S \subseteq X) \to ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x) = X ∖ ⋃_{x \in J \cap 𝒫 (X ∖ S)} x$
63	54 62	eqtr4d	$⊢ (J \in Top \land S \subseteq X) \to X ∖ ⋃ (J \cap 𝒫 (X ∖ S)) = ⋂_{x \in J \cap 𝒫 (X ∖ S)} (X ∖ x)$
64	50 51 63	3eqtr4d	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = X ∖ ⋃ (J \cap 𝒫 (X ∖ S))$
65		difssd	$⊢ S \subseteq X \to X ∖ S \subseteq X$
66	1	ntrval	$⊢ (J \in Top \land X ∖ S \subseteq X) \to int (J) (X ∖ S) = ⋃ (J \cap 𝒫 (X ∖ S))$
67	65 66	sylan2	$⊢ (J \in Top \land S \subseteq X) \to int (J) (X ∖ S) = ⋃ (J \cap 𝒫 (X ∖ S))$
68	67	difeq2d	$⊢ (J \in Top \land S \subseteq X) \to X ∖ int (J) (X ∖ S) = X ∖ ⋃ (J \cap 𝒫 (X ∖ S))$
69	64 68	eqtr4d	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = X ∖ int (J) (X ∖ S)$

Metamath Proof Explorer

Theorem clsval2

Proof