Metamath Proof Explorer


Theorem ntrcls0

Description: A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007)

Ref Expression
Hypothesis clscld.1 X=J
Assertion ntrcls0 JTopSXintJclsJS=intJS=

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 simpl JTopSXJTop
3 1 clsss3 JTopSXclsJSX
4 1 sscls JTopSXSclsJS
5 1 ntrss JTopclsJSXSclsJSintJSintJclsJS
6 2 3 4 5 syl3anc JTopSXintJSintJclsJS
7 6 3adant3 JTopSXintJclsJS=intJSintJclsJS
8 sseq2 intJclsJS=intJSintJclsJSintJS
9 8 3ad2ant3 JTopSXintJclsJS=intJSintJclsJSintJS
10 7 9 mpbid JTopSXintJclsJS=intJS
11 ss0 intJSintJS=
12 10 11 syl JTopSXintJclsJS=intJS=