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 ⊢ 𝑋 = ∪ 𝐽
Assertion ntrcls0 ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝐽 ∈ Top )
3 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
4 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
5 1 ntrss ⊢ ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ∧ 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
6 2 3 4 5 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
7 6 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
8 sseq2 ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∅ ) )
9 8 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∅ ) )
10 7 9 mpbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∅ )
11 ss0 ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∅ → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ )
12 10 11 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ )