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 JTopAXclsJXA=XintJA

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 difss XAX
3 1 clsval2 JTopXAXclsJXA=XintJXXA
4 2 3 mpan2 JTopclsJXA=XintJXXA
5 4 adantr JTopAXclsJXA=XintJXXA
6 simpr JTopAXAX
7 dfss4 AXXXA=A
8 6 7 sylib JTopAXXXA=A
9 8 fveq2d JTopAXintJXXA=intJA
10 9 difeq2d JTopAXXintJXXA=XintJA
11 5 10 eqtrd JTopAXclsJXA=XintJA