Theorem isopn2

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

	Ref	Expression
Hypothesis	iscld.1	$$⊢X=\bigcup J$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2		difss	$$⊢X\setminus S\subseteq X$$
3	1	iscld2	$$⊢\left(J\in \mathrm{Top}\wedge X\setminus S\subseteq X\right)\to \left(X\setminus S\in \mathrm{Clsd}\left(J\right)\leftrightarrow X\setminus \left(X\setminus S\right)\in J\right)$$
4	2 3	mpan2	$$⊢J\in \mathrm{Top}\to \left(X\setminus S\in \mathrm{Clsd}\left(J\right)\leftrightarrow X\setminus \left(X\setminus S\right)\in J\right)$$
5		dfss4	$$⊢S\subseteq X\leftrightarrow X\setminus \left(X\setminus S\right)=S$$
6	5	biimpi	$$⊢S\subseteq X\to X\setminus \left(X\setminus S\right)=S$$
7	6	eleq1d	$$⊢S\subseteq X\to \left(X\setminus \left(X\setminus S\right)\in J\leftrightarrow S\in J\right)$$
8	4 7	sylan9bb	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \left(X\setminus S\in \mathrm{Clsd}\left(J\right)\leftrightarrow S\in J\right)$$
9	8	bicomd	$$⊢\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)$$