Theorem iscld

Description: The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2	1	cldval	$$⊢J\in \mathrm{Top}\to \mathrm{Clsd}\left(J\right)=\left\{x\in 𝒫X|X\setminus x\in J\right\}$$
3	2	eleq2d	$$⊢J\in \mathrm{Top}\to \left(S\in \mathrm{Clsd}\left(J\right)\leftrightarrow S\in \left\{x\in 𝒫X|X\setminus x\in J\right\}\right)$$
4		difeq2	$$⊢x=S\to X\setminus x=X\setminus S$$
5	4	eleq1d	$$⊢x=S\to \left(X\setminus x\in J\leftrightarrow X\setminus S\in J\right)$$
6	5	elrab	$$⊢S\in \left\{x\in 𝒫X|X\setminus x\in J\right\}\leftrightarrow \left(S\in 𝒫X\wedge X\setminus S\in J\right)$$
7	3 6	bitrdi	$$⊢J\in \mathrm{Top}\to \left(S\in \mathrm{Clsd}\left(J\right)\leftrightarrow \left(S\in 𝒫X\wedge X\setminus S\in J\right)\right)$$
8	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
9		elpw2g	$$⊢X\in J\to \left(S\in 𝒫X\leftrightarrow S\subseteq X\right)$$
10	8 9	syl	$$⊢J\in \mathrm{Top}\to \left(S\in 𝒫X\leftrightarrow S\subseteq X\right)$$
11	10	anbi1d	$$⊢J\in \mathrm{Top}\to \left(\left(S\in 𝒫X\wedge X\setminus S\in J\right)\leftrightarrow \left(S\subseteq X\wedge X\setminus S\in J\right)\right)$$
12	7 11	bitrd	$$⊢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)$$