Theorem clsdif

Description: A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009)

	Ref	Expression
Hypothesis	clscld.1	$$⊢X=\bigcup J$$
Assertion	clsdif	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(X\setminus A\right)=X\setminus \mathrm{int}\left(J\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$$⊢X=\bigcup J$$
2		difss	$$⊢X\setminus A\subseteq X$$
3	1	clsval2	$$⊢\left(J\in \mathrm{Top}\wedge X\setminus A\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(X\setminus A\right)=X\setminus \mathrm{int}\left(J\right)\left(X\setminus \left(X\setminus A\right)\right)$$
4	2 3	mpan2	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)\left(X\setminus A\right)=X\setminus \mathrm{int}\left(J\right)\left(X\setminus \left(X\setminus A\right)\right)$$
5	4	adantr	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(X\setminus A\right)=X\setminus \mathrm{int}\left(J\right)\left(X\setminus \left(X\setminus A\right)\right)$$
6		simpr	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to A\subseteq X$$
7		dfss4	$$⊢A\subseteq X\leftrightarrow X\setminus \left(X\setminus A\right)=A$$
8	6 7	sylib	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to X\setminus \left(X\setminus A\right)=A$$
9	8	fveq2d	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{int}\left(J\right)\left(X\setminus \left(X\setminus A\right)\right)=\mathrm{int}\left(J\right)\left(A\right)$$
10	9	difeq2d	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to X\setminus \mathrm{int}\left(J\right)\left(X\setminus \left(X\setminus A\right)\right)=X\setminus \mathrm{int}\left(J\right)\left(A\right)$$
11	5 10	eqtrd	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(X\setminus A\right)=X\setminus \mathrm{int}\left(J\right)\left(A\right)$$