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 = U. J
Assertion clsdif 
|- ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 difss 
 |-  ( X \ A ) C_ X
3 1 clsval2 
 |-  ( ( J e. Top /\ ( X \ A ) C_ X ) -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` ( X \ ( X \ A ) ) ) ) )
4 2 3 mpan2 
 |-  ( J e. Top -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` ( X \ ( X \ A ) ) ) ) )
5 4 adantr 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` ( X \ ( X \ A ) ) ) ) )
6 simpr 
 |-  ( ( J e. Top /\ A C_ X ) -> A C_ X )
7 dfss4 
 |-  ( A C_ X <-> ( X \ ( X \ A ) ) = A )
8 6 7 sylib 
 |-  ( ( J e. Top /\ A C_ X ) -> ( X \ ( X \ A ) ) = A )
9 8 fveq2d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` ( X \ ( X \ A ) ) ) = ( ( int ` J ) ` A ) )
10 9 difeq2d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( X \ ( ( int ` J ) ` ( X \ ( X \ A ) ) ) ) = ( X \ ( ( int ` J ) ` A ) ) )
11 5 10 eqtrd 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` A ) ) )