Metamath Proof Explorer


Theorem ntrval2

Description: Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007)

Ref Expression
Hypothesis clscld.1 X=J
Assertion ntrval2 JTopSXintJS=XclsJXS

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 difss XSX
3 1 clsval2 JTopXSXclsJXS=XintJXXS
4 2 3 mpan2 JTopclsJXS=XintJXXS
5 4 adantr JTopSXclsJXS=XintJXXS
6 dfss4 SXXXS=S
7 6 biimpi SXXXS=S
8 7 fveq2d SXintJXXS=intJS
9 8 adantl JTopSXintJXXS=intJS
10 9 difeq2d JTopSXXintJXXS=XintJS
11 5 10 eqtrd JTopSXclsJXS=XintJS
12 11 difeq2d JTopSXXclsJXS=XXintJS
13 1 ntropn JTopSXintJSJ
14 1 eltopss JTopintJSJintJSX
15 13 14 syldan JTopSXintJSX
16 dfss4 intJSXXXintJS=intJS
17 15 16 sylib JTopSXXXintJS=intJS
18 12 17 eqtr2d JTopSXintJS=XclsJXS