Theorem iscld2

Description: A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2	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)$$
3	2	baibd	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \left(S\in \mathrm{Clsd}\left(J\right)\leftrightarrow X\setminus S\in J\right)$$