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		incom	$⊢ (X ∖ A) \cap A = A \cap (X ∖ A)$
10		disjdif	$⊢ A \cap (X ∖ A) = \emptyset$
11	9 10	eqtri	$⊢ (X ∖ A) \cap A = \emptyset$
12		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$
13	8 11 12	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$
14	13	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)$
15		incom	$⊢ cls (J) (A) \cap cls (J) (X ∖ A) = cls (J) (X ∖ A) \cap cls (J) (A)$
16		dfss4	$⊢ A \subseteq X \leftrightarrow X ∖ (X ∖ A) = A$
17		fveq2	$⊢ X ∖ (X ∖ A) = A \to cls (J) (X ∖ (X ∖ A)) = cls (J) (A)$
18	17	eqcomd	$⊢ X ∖ (X ∖ A) = A \to cls (J) (A) = cls (J) (X ∖ (X ∖ A))$
19	16 18	sylbi	$⊢ A \subseteq X \to cls (J) (A) = cls (J) (X ∖ (X ∖ A))$
20	19	adantl	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) = cls (J) (X ∖ (X ∖ A))$
21	20	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))$
22	15 21	syl5eq	$⊢ (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))$
23	22	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)))$
24	23	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)$
25		difss	$⊢ X ∖ A \subseteq X$
26	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)$
27	25 26	mpan2	$⊢ J \in Top \to (X ∖ A \in J \leftrightarrow (X ∖ A) \cap (cls (J) (X ∖ A) \cap cls (J) (X ∖ (X ∖ A))) = \emptyset)$
28	27	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)$
29	24 28	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)$
30	1	opncld	$⊢ (J \in Top \land X ∖ A \in J) \to X ∖ (X ∖ A) \in Clsd (J)$
31	30	ex	$⊢ J \in Top \to (X ∖ A \in J \to X ∖ (X ∖ A) \in Clsd (J))$
32	31	adantr	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ A \in J \to X ∖ (X ∖ A) \in Clsd (J))$
33		eleq1	$⊢ X ∖ (X ∖ A) = A \to (X ∖ (X ∖ A) \in Clsd (J) \leftrightarrow A \in Clsd (J))$
34	16 33	sylbi	$⊢ A \subseteq X \to (X ∖ (X ∖ A) \in Clsd (J) \leftrightarrow A \in Clsd (J))$
35	34	adantl	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ (X ∖ A) \in Clsd (J) \leftrightarrow A \in Clsd (J))$
36	32 35	sylibd	$⊢ (J \in Top \land A \subseteq X) \to (X ∖ A \in J \to A \in Clsd (J))$
37	29 36	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))$
38	14 37	syld	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (A) \cap cls (J) (X ∖ A) \subseteq A \to A \in Clsd (J))$
39	6 38	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