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

Metamath Proof Explorer

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