This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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