Metamath Proof Explorer


Theorem clsdif

Description: A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009)

Ref Expression
Hypothesis clscld.1 X = J
Assertion clsdif J Top A X cls J X A = X int J A

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 difss X A X
3 1 clsval2 J Top X A X cls J X A = X int J X X A
4 2 3 mpan2 J Top cls J X A = X int J X X A
5 4 adantr J Top A X cls J X A = X int J X X A
6 simpr J Top A X A X
7 dfss4 A X X X A = A
8 6 7 sylib J Top A X X X A = A
9 8 fveq2d J Top A X int J X X A = int J A
10 9 difeq2d J Top A X X int J X X A = X int J A
11 5 10 eqtrd J Top A X cls J X A = X int J A