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=J
Assertion cmclsopn JTopSXXclsJSJ

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 1 clsval2 JTopSXclsJS=XintJXS
3 2 difeq2d JTopSXXclsJS=XXintJXS
4 difss XSX
5 1 ntropn JTopXSXintJXSJ
6 4 5 mpan2 JTopintJXSJ
7 1 eltopss JTopintJXSJintJXSX
8 6 7 mpdan JTopintJXSX
9 dfss4 intJXSXXXintJXS=intJXS
10 8 9 sylib JTopXXintJXS=intJXS
11 10 6 eqeltrd JTopXXintJXSJ
12 11 adantr JTopSXXXintJXSJ
13 3 12 eqeltrd JTopSXXclsJSJ