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 )