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}=\bigcup {J}$
Assertion ntrcls0 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing \right)\to \mathrm{int}\left({J}\right)\left({S}\right)=\varnothing$

Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 simpl ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {J}\in \mathrm{Top}$
3 1 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}$
4 1 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$
5 1 ntrss ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}\wedge {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \mathrm{int}\left({J}\right)\left({S}\right)\subseteq \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)$
6 2 3 4 5 syl3anc ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{int}\left({J}\right)\left({S}\right)\subseteq \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)$
7 6 3adant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing \right)\to \mathrm{int}\left({J}\right)\left({S}\right)\subseteq \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)$
8 sseq2 ${⊢}\mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing \to \left(\mathrm{int}\left({J}\right)\left({S}\right)\subseteq \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)↔\mathrm{int}\left({J}\right)\left({S}\right)\subseteq \varnothing \right)$
9 8 3ad2ant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing \right)\to \left(\mathrm{int}\left({J}\right)\left({S}\right)\subseteq \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)↔\mathrm{int}\left({J}\right)\left({S}\right)\subseteq \varnothing \right)$
10 7 9 mpbid ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing \right)\to \mathrm{int}\left({J}\right)\left({S}\right)\subseteq \varnothing$
11 ss0 ${⊢}\mathrm{int}\left({J}\right)\left({S}\right)\subseteq \varnothing \to \mathrm{int}\left({J}\right)\left({S}\right)=\varnothing$
12 10 11 syl ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge \mathrm{int}\left({J}\right)\left(\mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing \right)\to \mathrm{int}\left({J}\right)\left({S}\right)=\varnothing$