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 ( 𝐴𝑉 → ( Clsd ‘ 𝒫 𝐴 ) = 𝒫 𝐴 )

Proof

Step Hyp Ref Expression
1 difss ( 𝐴𝑥 ) ⊆ 𝐴
2 elpw2g ( 𝐴𝑉 → ( ( 𝐴𝑥 ) ∈ 𝒫 𝐴 ↔ ( 𝐴𝑥 ) ⊆ 𝐴 ) )
3 1 2 mpbiri ( 𝐴𝑉 → ( 𝐴𝑥 ) ∈ 𝒫 𝐴 )
4 distop ( 𝐴𝑉 → 𝒫 𝐴 ∈ Top )
5 unipw 𝒫 𝐴 = 𝐴
6 5 eqcomi 𝐴 = 𝒫 𝐴
7 6 iscld ( 𝒫 𝐴 ∈ Top → ( 𝑥 ∈ ( Clsd ‘ 𝒫 𝐴 ) ↔ ( 𝑥𝐴 ∧ ( 𝐴𝑥 ) ∈ 𝒫 𝐴 ) ) )
8 4 7 syl ( 𝐴𝑉 → ( 𝑥 ∈ ( Clsd ‘ 𝒫 𝐴 ) ↔ ( 𝑥𝐴 ∧ ( 𝐴𝑥 ) ∈ 𝒫 𝐴 ) ) )
9 3 8 mpbiran2d ( 𝐴𝑉 → ( 𝑥 ∈ ( Clsd ‘ 𝒫 𝐴 ) ↔ 𝑥𝐴 ) )
10 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
11 9 10 bitr4di ( 𝐴𝑉 → ( 𝑥 ∈ ( Clsd ‘ 𝒫 𝐴 ) ↔ 𝑥 ∈ 𝒫 𝐴 ) )
12 11 eqrdv ( 𝐴𝑉 → ( Clsd ‘ 𝒫 𝐴 ) = 𝒫 𝐴 )