opnbnd

Description: A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		opnbnd.1	$⊢ X = ⋃ J$
2		disjdif	$⊢ int (J) (A) \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset$
3	2	a1i	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset$
4		ineq1	$⊢ int (J) (A) = A \to int (J) (A) \cap (cls (J) (A) ∖ int (J) (A)) = A \cap (cls (J) (A) ∖ int (J) (A))$
5	4	eqeq1d	$⊢ int (J) (A) = A \to (int (J) (A) \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset \leftrightarrow A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset)$
6	3 5	syl5ibcom	$⊢ (J \in Top \land A \subseteq X) \to (int (J) (A) = A \to A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset)$
7	1	ntrss2	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \subseteq A$
8	7	adantr	$⊢ ((J \in Top \land A \subseteq X) \land A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset) \to int (J) (A) \subseteq A$
9		inssdif0	$⊢ A \cap cls (J) (A) \subseteq int (J) (A) \leftrightarrow A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset$
10	1	sscls	$⊢ (J \in Top \land A \subseteq X) \to A \subseteq cls (J) (A)$
11		df-ss	$⊢ A \subseteq cls (J) (A) \leftrightarrow A \cap cls (J) (A) = A$
12	10 11	sylib	$⊢ (J \in Top \land A \subseteq X) \to A \cap cls (J) (A) = A$
13	12	eqcomd	$⊢ (J \in Top \land A \subseteq X) \to A = A \cap cls (J) (A)$
14		eqimss	$⊢ A = A \cap cls (J) (A) \to A \subseteq A \cap cls (J) (A)$
15	13 14	syl	$⊢ (J \in Top \land A \subseteq X) \to A \subseteq A \cap cls (J) (A)$
16		sstr	$⊢ (A \subseteq A \cap cls (J) (A) \land A \cap cls (J) (A) \subseteq int (J) (A)) \to A \subseteq int (J) (A)$
17	15 16	sylan	$⊢ ((J \in Top \land A \subseteq X) \land A \cap cls (J) (A) \subseteq int (J) (A)) \to A \subseteq int (J) (A)$
18	9 17	sylan2br	$⊢ ((J \in Top \land A \subseteq X) \land A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset) \to A \subseteq int (J) (A)$
19	8 18	eqssd	$⊢ ((J \in Top \land A \subseteq X) \land A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset) \to int (J) (A) = A$
20	19	ex	$⊢ (J \in Top \land A \subseteq X) \to (A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset \to int (J) (A) = A)$
21	6 20	impbid	$⊢ (J \in Top \land A \subseteq X) \to (int (J) (A) = A \leftrightarrow A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset)$
22	1	isopn3	$⊢ (J \in Top \land A \subseteq X) \to (A \in J \leftrightarrow int (J) (A) = A)$
23	1	topbnd	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \cap cls (J) (X ∖ A) = cls (J) (A) ∖ int (J) (A)$
24	23	ineq2d	$⊢ (J \in Top \land A \subseteq X) \to A \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = A \cap (cls (J) (A) ∖ int (J) (A))$
25	24	eqeq1d	$⊢ (J \in Top \land A \subseteq X) \to (A \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset \leftrightarrow A \cap (cls (J) (A) ∖ int (J) (A)) = \emptyset)$
26	21 22 25	3bitr4d	$⊢ (J \in Top \land A \subseteq X) \to (A \in J \leftrightarrow A \cap (cls (J) (A) \cap cls (J) (X ∖ A)) = \emptyset)$

Metamath Proof Explorer

Theorem opnbnd

Proof