topbnd

Description: Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009)

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

Step	Hyp	Ref	Expression
1		topbnd.1	$⊢ X = ⋃ J$
2	1	clsdif	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (X ∖ A) = X ∖ int (J) (A)$
3	2	ineq2d	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \cap cls (J) (X ∖ A) = cls (J) (A) \cap (X ∖ int (J) (A))$
4		indif2	$⊢ cls (J) (A) \cap (X ∖ int (J) (A)) = (cls (J) (A) \cap X) ∖ int (J) (A)$
5	3 4	eqtrdi	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \cap cls (J) (X ∖ A) = (cls (J) (A) \cap X) ∖ int (J) (A)$
6	1	clsss3	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \subseteq X$
7		df-ss	$⊢ cls (J) (A) \subseteq X \leftrightarrow cls (J) (A) \cap X = cls (J) (A)$
8	6 7	sylib	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \cap X = cls (J) (A)$
9	8	difeq1d	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (A) \cap X) ∖ int (J) (A) = cls (J) (A) ∖ int (J) (A)$
10	5 9	eqtrd	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \cap cls (J) (X ∖ A) = cls (J) (A) ∖ int (J) (A)$

Metamath Proof Explorer