cldbnd

Description: A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009)

		Ref	Expression
	Hypothesis	opnbnd.1	$⊢ X = ⋃ J$
	Assertion	cldbnd	$⊢ (J \in Top \land A \subseteq X) \to (A \in Clsd (J) \leftrightarrow cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		opnbnd.1	$⊢ X = ⋃ J$
2	1	iscld3	$⊢ (J \in Top \land A \subseteq X) \to (A \in Clsd (J) \leftrightarrow cls (J) (A) = A)$
3		eqimss	$⊢ cls (J) (A) = A \to cls (J) (A) \subseteq A$
4	2 3	syl6bi	$⊢ (J \in Top \land A \subseteq X) \to (A \in Clsd (J) \to cls (J) (A) \subseteq A)$
5		ssinss1	$⊢ cls (J) (A) \subseteq A \to cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A$
6	4 5	syl6	$⊢ (J \in Top \land A \subseteq X) \to (A \in Clsd (J) \to cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A)$
7		sslin	$⊢ cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A \to (X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) \subseteq (X ∖ A) \cap A$
8	7	adantl	$⊢ ((J \in Top \land A \subseteq X) \land cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A) \to (X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) \subseteq (X ∖ A) \cap A$
9		disjdifr	$⊢ (X ∖ A) \cap A = \emptyset$
10		sseq0	$⊢ ((X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) \subseteq (X ∖ A) \cap A \land (X ∖ A) \cap A = \emptyset) \to (X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset$
11	8 9 10	sylancl	$⊢ ((J \in Top \land A \subseteq X) \land cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A) \to (X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset$
12	11	ex	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A \to (X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset)$
13		incom	$⊢ cls (J) (A) \cap cls (J) (X ∖ A) = cls (J) (X ∖ A) \cap cls (J) (A)$
14		dfss4	$⊢ A \subseteq X \leftrightarrow X ∖ (X ∖ A) = A$
15		fveq2	$⊢ X ∖ (X ∖ A) = A \to cls (J) (X ∖ (X ∖ A)) = cls (J) (A)$
16	15	eqcomd	$⊢ X ∖ (X ∖ A) = A \to cls (J) (A) = cls (J) (X ∖ (X ∖ A))$
17	14 16	sylbi	$⊢ A \subseteq X \to cls (J) (A) = cls (J) (X ∖ (X ∖ A))$
18	17	adantl	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) = cls (J) (X ∖ (X ∖ A))$
19	18	ineq2d	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (X ∖ A) \cap cls (J) (A) = cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))$
20	13 19	eqtrid	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \cap cls (J) (X ∖ A) = cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))$
21	20	ineq2d	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = (X ∖ A) \cap (cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A)))$
22	21	eqeq1d	$⊢ (J \in Top \land A \subseteq X) \to ((X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset \leftrightarrow (X ∖ A) \cap (cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))) = \emptyset)$
23		difss	$⊢ X ∖ A \subseteq X$
24	1	opnbnd	$⊢ (J \in Top \land X ∖ A \subseteq X) \to (X ∖ A \in J \leftrightarrow (X ∖ A) \cap (cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))) = \emptyset)$
25	23 24	mpan2	$⊢ J \in Top \to (X ∖ A \in J \leftrightarrow (X ∖ A) \cap (cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))) = \emptyset)$
26	25	adantr	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ A \in J \leftrightarrow (X ∖ A) \cap (cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))) = \emptyset)$
27	22 26	bitr4d	$⊢ (J \in Top \land A \subseteq X) \to ((X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset \leftrightarrow X ∖ A \in J)$
28	1	opncld	$⊢ (J \in Top \land X ∖ A \in J) \to X ∖ (X ∖ A) \in Clsd (J)$
29	28	ex	$⊢ J \in Top \to (X ∖ A \in J \to X ∖ (X ∖ A) \in Clsd (J))$
30	29	adantr	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ A \in J \to X ∖ (X ∖ A) \in Clsd (J))$
31		eleq1	$⊢ X ∖ (X ∖ A) = A \to (X ∖ (X ∖ A) \in Clsd (J) \leftrightarrow A \in Clsd (J))$
32	14 31	sylbi	$⊢ A \subseteq X \to (X ∖ (X ∖ A) \in Clsd (J) \leftrightarrow A \in Clsd (J))$
33	32	adantl	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ (X ∖ A) \in Clsd (J) \leftrightarrow A \in Clsd (J))$
34	30 33	sylibd	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ A \in J \to A \in Clsd (J))$
35	27 34	sylbid	$⊢ (J \in Top \land A \subseteq X) \to ((X ∖ A) \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset \to A \in Clsd (J))$
36	12 35	syld	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A \to A \in Clsd (J))$
37	6 36	impbid	$⊢ (J \in Top \land A \subseteq X) \to (A \in Clsd (J) \leftrightarrow cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A)$

Metamath Proof Explorer

Theorem cldbnd

Proof