Metamath Proof Explorer

Theorem ntrss

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

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion ntrss 
|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( int ` J ) ` T ) C_ ( ( int ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 sscon 
 |-  ( T C_ S -> ( X \ S ) C_ ( X \ T ) )
3 2 adantl 
 |-  ( ( S C_ X /\ T C_ S ) -> ( X \ S ) C_ ( X \ T ) )
4 difss 
 |-  ( X \ T ) C_ X
5 3 4 jctil 
 |-  ( ( S C_ X /\ T C_ S ) -> ( ( X \ T ) C_ X /\ ( X \ S ) C_ ( X \ T ) ) )
6 1 clsss 
 |-  ( ( J e. Top /\ ( X \ T ) C_ X /\ ( X \ S ) C_ ( X \ T ) ) -> ( ( cls ` J ) ` ( X \ S ) ) C_ ( ( cls ` J ) ` ( X \ T ) ) )
7 6 3expb 
 |-  ( ( J e. Top /\ ( ( X \ T ) C_ X /\ ( X \ S ) C_ ( X \ T ) ) ) -> ( ( cls ` J ) ` ( X \ S ) ) C_ ( ( cls ` J ) ` ( X \ T ) ) )
8 5 7 sylan2 
 |-  ( ( J e. Top /\ ( S C_ X /\ T C_ S ) ) -> ( ( cls ` J ) ` ( X \ S ) ) C_ ( ( cls ` J ) ` ( X \ T ) ) )
9 8 sscond 
 |-  ( ( J e. Top /\ ( S C_ X /\ T C_ S ) ) -> ( X \ ( ( cls ` J ) ` ( X \ T ) ) ) C_ ( X \ ( ( cls ` J ) ` ( X \ S ) ) ) )
10 sstr2 
 |-  ( T C_ S -> ( S C_ X -> T C_ X ) )
11 10 impcom 
 |-  ( ( S C_ X /\ T C_ S ) -> T C_ X )
12 1 ntrval2 
 |-  ( ( J e. Top /\ T C_ X ) -> ( ( int ` J ) ` T ) = ( X \ ( ( cls ` J ) ` ( X \ T ) ) ) )
13 11 12 sylan2 
 |-  ( ( J e. Top /\ ( S C_ X /\ T C_ S ) ) -> ( ( int ` J ) ` T ) = ( X \ ( ( cls ` J ) ` ( X \ T ) ) ) )
14 1 ntrval2 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = ( X \ ( ( cls ` J ) ` ( X \ S ) ) ) )
15 14 adantrr 
 |-  ( ( J e. Top /\ ( S C_ X /\ T C_ S ) ) -> ( ( int ` J ) ` S ) = ( X \ ( ( cls ` J ) ` ( X \ S ) ) ) )
16 9 13 15 3sstr4d 
 |-  ( ( J e. Top /\ ( S C_ X /\ T C_ S ) ) -> ( ( int ` J ) ` T ) C_ ( ( int ` J ) ` S ) )
17 16 3impb 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( int ` J ) ` T ) C_ ( ( int ` J ) ` S ) )