Theorem difopn

Description: The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014)

	Ref	Expression
Hypothesis	iscld.1	$$⊢X=\bigcup J$$
Assertion	difopn	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\setminus B\in J$$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2		elssuni	$$⊢A\in J\to A\subseteq \bigcup J$$
3	2 1	sseqtrrdi	$$⊢A\in J\to A\subseteq X$$
4	3	adantr	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\subseteq X$$
5		df-ss	$$⊢A\subseteq X\leftrightarrow A\cap X=A$$
6	4 5	sylib	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\cap X=A$$
7	6	difeq1d	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to \left(A\cap X\right)\setminus B=A\setminus B$$
8		indif2	$$⊢A\cap \left(X\setminus B\right)=\left(A\cap X\right)\setminus B$$
9		cldrcl	$$⊢B\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
10	9	adantl	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to J\in \mathrm{Top}$$
11		simpl	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\in J$$
12	1	cldopn	$$⊢B\in \mathrm{Clsd}\left(J\right)\to X\setminus B\in J$$
13	12	adantl	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to X\setminus B\in J$$
14		inopn	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge X\setminus B\in J\right)\to A\cap \left(X\setminus B\right)\in J$$
15	10 11 13 14	syl3anc	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\cap \left(X\setminus B\right)\in J$$
16	8 15	eqeltrrid	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to \left(A\cap X\right)\setminus B\in J$$
17	7 16	eqeltrrd	$$⊢\left(A\in J\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\setminus B\in J$$