Metamath Proof Explorer

Theorem cmclsopn

Description: The complement of a closure is open. (Contributed by NM, 11-Sep-2006)

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion cmclsopn 
|- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( cls ` J ) ` S ) ) e. J )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 1 clsval2 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( X \ ( ( int ` J ) ` ( X \ S ) ) ) )
3 2 difeq2d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( cls ` J ) ` S ) ) = ( X \ ( X \ ( ( int ` J ) ` ( X \ S ) ) ) ) )
4 difss 
 |-  ( X \ S ) C_ X
5 1 ntropn 
 |-  ( ( J e. Top /\ ( X \ S ) C_ X ) -> ( ( int ` J ) ` ( X \ S ) ) e. J )
6 4 5 mpan2 
 |-  ( J e. Top -> ( ( int ` J ) ` ( X \ S ) ) e. J )
7 1 eltopss 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` ( X \ S ) ) e. J ) -> ( ( int ` J ) ` ( X \ S ) ) C_ X )
8 6 7 mpdan 
 |-  ( J e. Top -> ( ( int ` J ) ` ( X \ S ) ) C_ X )
9 dfss4 
 |-  ( ( ( int ` J ) ` ( X \ S ) ) C_ X <-> ( X \ ( X \ ( ( int ` J ) ` ( X \ S ) ) ) ) = ( ( int ` J ) ` ( X \ S ) ) )
10 8 9 sylib 
 |-  ( J e. Top -> ( X \ ( X \ ( ( int ` J ) ` ( X \ S ) ) ) ) = ( ( int ` J ) ` ( X \ S ) ) )
11 10 6 eqeltrd 
 |-  ( J e. Top -> ( X \ ( X \ ( ( int ` J ) ` ( X \ S ) ) ) ) e. J )
12 11 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> ( X \ ( X \ ( ( int ` J ) ` ( X \ S ) ) ) ) e. J )
13 3 12 eqeltrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( cls ` J ) ` S ) ) e. J )