Theorem ntrss

Description: Subset relationship for interior. (Contributed by NM, 3-Oct-2007)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		sscon	⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑋 ∖ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑇 ) )
3	2	adantl	⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑋 ∖ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑇 ) )
4		difss	⊢ ( 𝑋 ∖ 𝑇 ) ⊆ 𝑋
5	3 4	jctil	⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( ( 𝑋 ∖ 𝑇 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑇 ) ) )
6	1	clsss	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝑇 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑇 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑇 ) ) )
7	6	3expb	⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑋 ∖ 𝑇 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑇 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑇 ) ) )
8	5 7	sylan2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑇 ) ) )
9	8	sscond	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑇 ) ) ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )
10		sstr2	⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑋 → 𝑇 ⊆ 𝑋 ) )
11	10	impcom	⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑋 )
12	1	ntrval2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑇 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑇 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑇 ) ) ) )
13	11 12	sylan2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑇 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑇 ) ) ) )
14	1	ntrval2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )
15	14	adantrr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )
16	9 13 15	3sstr4d	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
17	16	3impb	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( ( int ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )