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 ‘ 𝐽 ) ‘ 𝑆 ) = ∅ )