Theorem cldopn

Description: The complement of a closed set is open. (Contributed by NM, 5-Oct-2006) (Revised by Stefan O'Rear, 22-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2		cldrcl	$$⊢S\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
3	1	iscld	$$⊢J\in \mathrm{Top}\to \left(S\in \mathrm{Clsd}\left(J\right)\leftrightarrow \left(S\subseteq X\wedge X\setminus S\in J\right)\right)$$
4	3	simplbda	$$⊢\left(J\in \mathrm{Top}\wedge S\in \mathrm{Clsd}\left(J\right)\right)\to X\setminus S\in J$$
5	2 4	mpancom	$$⊢S\in \mathrm{Clsd}\left(J\right)\to X\setminus S\in J$$