Metamath Proof Explorer


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 V Clsd 𝒫 A = 𝒫 A

Proof

Step Hyp Ref Expression
1 difss A x A
2 elpw2g A V A x 𝒫 A A x A
3 1 2 mpbiri A V A x 𝒫 A
4 distop A V 𝒫 A Top
5 unipw 𝒫 A = A
6 5 eqcomi A = 𝒫 A
7 6 iscld 𝒫 A Top x Clsd 𝒫 A x A A x 𝒫 A
8 4 7 syl A V x Clsd 𝒫 A x A A x 𝒫 A
9 3 8 mpbiran2d A V x Clsd 𝒫 A x A
10 velpw x 𝒫 A x A
11 9 10 bitr4di A V x Clsd 𝒫 A x 𝒫 A
12 11 eqrdv A V Clsd 𝒫 A = 𝒫 A