This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ J ∈ Top ∧ S ⊆ X ∧ int ⁡ J ⁡ cls ⁡ J ⁡ S = ∅ → int ⁡ J ⁡ S = ∅

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 simpl ⊢ J ∈ Top ∧ S ⊆ X → J ∈ Top
3 1 clsss3 ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ X
4 1 sscls ⊢ J ∈ Top ∧ S ⊆ X → S ⊆ cls ⁡ J ⁡ S
5 1 ntrss ⊢ J ∈ Top ∧ cls ⁡ J ⁡ S ⊆ X ∧ S ⊆ cls ⁡ J ⁡ S → int ⁡ J ⁡ S ⊆ int ⁡ J ⁡ cls ⁡ J ⁡ S
6 2 3 4 5 syl3anc ⊢ J ∈ Top ∧ S ⊆ X → int ⁡ J ⁡ S ⊆ int ⁡ J ⁡ cls ⁡ J ⁡ S
7 6 3adant3 ⊢ J ∈ Top ∧ S ⊆ X ∧ int ⁡ J ⁡ cls ⁡ J ⁡ S = ∅ → int ⁡ J ⁡ S ⊆ int ⁡ J ⁡ cls ⁡ J ⁡ S
8 sseq2 ⊢ int ⁡ J ⁡ cls ⁡ J ⁡ S = ∅ → int ⁡ J ⁡ S ⊆ int ⁡ J ⁡ cls ⁡ J ⁡ S ↔ int ⁡ J ⁡ S ⊆ ∅
9 8 3ad2ant3 ⊢ J ∈ Top ∧ S ⊆ X ∧ int ⁡ J ⁡ cls ⁡ J ⁡ S = ∅ → int ⁡ J ⁡ S ⊆ int ⁡ J ⁡ cls ⁡ J ⁡ S ↔ int ⁡ J ⁡ S ⊆ ∅
10 7 9 mpbid ⊢ J ∈ Top ∧ S ⊆ X ∧ int ⁡ J ⁡ cls ⁡ J ⁡ S = ∅ → int ⁡ J ⁡ S ⊆ ∅
11 ss0 ⊢ int ⁡ J ⁡ S ⊆ ∅ → int ⁡ J ⁡ S = ∅
12 10 11 syl ⊢ J ∈ Top ∧ S ⊆ X ∧ int ⁡ J ⁡ cls ⁡ J ⁡ S = ∅ → int ⁡ J ⁡ S = ∅