Metamath Proof Explorer


Theorem ntrss

Description: Subset relationship for interior. (Contributed by NM, 3-Oct-2007)

Ref Expression
Hypothesis clscld.1 X=J
Assertion ntrss JTopSXTSintJTintJS

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 sscon TSXSXT
3 2 adantl SXTSXSXT
4 difss XTX
5 3 4 jctil SXTSXTXXSXT
6 1 clsss JTopXTXXSXTclsJXSclsJXT
7 6 3expb JTopXTXXSXTclsJXSclsJXT
8 5 7 sylan2 JTopSXTSclsJXSclsJXT
9 8 sscond JTopSXTSXclsJXTXclsJXS
10 sstr2 TSSXTX
11 10 impcom SXTSTX
12 1 ntrval2 JTopTXintJT=XclsJXT
13 11 12 sylan2 JTopSXTSintJT=XclsJXT
14 1 ntrval2 JTopSXintJS=XclsJXS
15 14 adantrr JTopSXTSintJS=XclsJXS
16 9 13 15 3sstr4d JTopSXTSintJTintJS
17 16 3impb JTopSXTSintJTintJS