Theorem ntrss2

Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	ntrss2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	ntrval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
3		inss2	⊢ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝒫 𝑆
4	3	unissi	⊢ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ ∪ 𝒫 𝑆
5		unipw	⊢ ∪ 𝒫 𝑆 = 𝑆
6	4 5	sseqtri	⊢ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆
7	2 6	eqsstrdi	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 )