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