Theorem opncld

Description: The complement of an open set is closed. (Contributed by NM, 6-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2		simpr	$$⊢\left(J\in \mathrm{Top}\wedge S\in J\right)\to S\in J$$
3	1	eltopss	$$⊢\left(J\in \mathrm{Top}\wedge S\in J\right)\to S\subseteq X$$
4	1	isopn2	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \left(S\in J\leftrightarrow X\setminus S\in \mathrm{Clsd}\left(J\right)\right)$$
5	3 4	syldan	$$⊢\left(J\in \mathrm{Top}\wedge S\in J\right)\to \left(S\in J\leftrightarrow X\setminus S\in \mathrm{Clsd}\left(J\right)\right)$$
6	2 5	mpbid	$$⊢\left(J\in \mathrm{Top}\wedge S\in J\right)\to X\setminus S\in \mathrm{Clsd}\left(J\right)$$