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 e. V -> ( Clsd ` ~P A ) = ~P A )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( A \ x ) C_ A
2 elpw2g 
 |-  ( A e. V -> ( ( A \ x ) e. ~P A <-> ( A \ x ) C_ A ) )
3 1 2 mpbiri 
 |-  ( A e. V -> ( A \ x ) e. ~P A )
4 distop 
 |-  ( A e. V -> ~P A e. Top )
5 unipw 
 |-  U. ~P A = A
6 5 eqcomi 
 |-  A = U. ~P A
7 6 iscld 
 |-  ( ~P A e. Top -> ( x e. ( Clsd ` ~P A ) <-> ( x C_ A /\ ( A \ x ) e. ~P A ) ) )
8 4 7 syl 
 |-  ( A e. V -> ( x e. ( Clsd ` ~P A ) <-> ( x C_ A /\ ( A \ x ) e. ~P A ) ) )
9 3 8 mpbiran2d 
 |-  ( A e. V -> ( x e. ( Clsd ` ~P A ) <-> x C_ A ) )
10 velpw 
 |-  ( x e. ~P A <-> x C_ A )
11 9 10 bitr4di 
 |-  ( A e. V -> ( x e. ( Clsd ` ~P A ) <-> x e. ~P A ) )
12 11 eqrdv 
 |-  ( A e. V -> ( Clsd ` ~P A ) = ~P A )