Metamath Proof Explorer

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 
|- X = U. J
Assertion ntrcls0 
|- ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( int ` J ) ` S ) = (/) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 simpl 
 |-  ( ( J e. Top /\ S C_ X ) -> J e. Top )
3 1 clsss3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
4 1 sscls 
 |-  ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
5 1 ntrss 
 |-  ( ( J e. Top /\ ( ( cls ` J ) ` S ) C_ X /\ S C_ ( ( cls ` J ) ` S ) ) -> ( ( int ` J ) ` S ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) )
6 2 3 4 5 syl3anc 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) )
7 6 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( int ` J ) ` S ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) )
8 sseq2 
 |-  ( ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) -> ( ( ( int ` J ) ` S ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) <-> ( ( int ` J ) ` S ) C_ (/) ) )
9 8 3ad2ant3 
 |-  ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( ( int ` J ) ` S ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) <-> ( ( int ` J ) ` S ) C_ (/) ) )
10 7 9 mpbid 
 |-  ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( int ` J ) ` S ) C_ (/) )
11 ss0 
 |-  ( ( ( int ` J ) ` S ) C_ (/) -> ( ( int ` J ) ` S ) = (/) )
12 10 11 syl 
 |-  ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( int ` J ) ` S ) = (/) )