Theorem discld

Description: The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007) (Revised by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Assertion	discld	$$⊢A\in V\to \mathrm{Clsd}\left(𝒫A\right)=𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢A\setminus x\subseteq A$$
2		elpw2g	$$⊢A\in V\to \left(A\setminus x\in 𝒫A\leftrightarrow A\setminus x\subseteq A\right)$$
3	1 2	mpbiri	$$⊢A\in V\to A\setminus x\in 𝒫A$$
4		distop	$$⊢A\in V\to 𝒫A\in \mathrm{Top}$$
5		unipw	$$⊢\bigcup 𝒫A=A$$
6	5	eqcomi	$$⊢A=\bigcup 𝒫A$$
7	6	iscld	$$⊢𝒫A\in \mathrm{Top}\to \left(x\in \mathrm{Clsd}\left(𝒫A\right)\leftrightarrow \left(x\subseteq A\wedge A\setminus x\in 𝒫A\right)\right)$$
8	4 7	syl	$$⊢A\in V\to \left(x\in \mathrm{Clsd}\left(𝒫A\right)\leftrightarrow \left(x\subseteq A\wedge A\setminus x\in 𝒫A\right)\right)$$
9	3 8	mpbiran2d	$$⊢A\in V\to \left(x\in \mathrm{Clsd}\left(𝒫A\right)\leftrightarrow x\subseteq A\right)$$
10		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
11	9 10	bitr4di	$$⊢A\in V\to \left(x\in \mathrm{Clsd}\left(𝒫A\right)\leftrightarrow x\in 𝒫A\right)$$
12	11	eqrdv	$$⊢A\in V\to \mathrm{Clsd}\left(𝒫A\right)=𝒫A$$