Metamath Proof Explorer

Theorem 0ntr

Description: A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 ssdif0 
 |-  ( X C_ S <-> ( X \ S ) = (/) )
3 eqss 
 |-  ( S = X <-> ( S C_ X /\ X C_ S ) )
4 fveq2 
 |-  ( S = X -> ( ( int ` J ) ` S ) = ( ( int ` J ) ` X ) )
5 1 ntrtop 
 |-  ( J e. Top -> ( ( int ` J ) ` X ) = X )
6 4 5 sylan9eqr 
 |-  ( ( J e. Top /\ S = X ) -> ( ( int ` J ) ` S ) = X )
7 6 eqeq1d 
 |-  ( ( J e. Top /\ S = X ) -> ( ( ( int ` J ) ` S ) = (/) <-> X = (/) ) )
8 7 biimpd 
 |-  ( ( J e. Top /\ S = X ) -> ( ( ( int ` J ) ` S ) = (/) -> X = (/) ) )
9 8 ex 
 |-  ( J e. Top -> ( S = X -> ( ( ( int ` J ) ` S ) = (/) -> X = (/) ) ) )
10 3 9 syl5bir 
 |-  ( J e. Top -> ( ( S C_ X /\ X C_ S ) -> ( ( ( int ` J ) ` S ) = (/) -> X = (/) ) ) )
11 10 expd 
 |-  ( J e. Top -> ( S C_ X -> ( X C_ S -> ( ( ( int ` J ) ` S ) = (/) -> X = (/) ) ) ) )
12 11 com34 
 |-  ( J e. Top -> ( S C_ X -> ( ( ( int ` J ) ` S ) = (/) -> ( X C_ S -> X = (/) ) ) ) )
13 12 imp32 
 |-  ( ( J e. Top /\ ( S C_ X /\ ( ( int ` J ) ` S ) = (/) ) ) -> ( X C_ S -> X = (/) ) )
14 2 13 syl5bir 
 |-  ( ( J e. Top /\ ( S C_ X /\ ( ( int ` J ) ` S ) = (/) ) ) -> ( ( X \ S ) = (/) -> X = (/) ) )
15 14 necon3d 
 |-  ( ( J e. Top /\ ( S C_ X /\ ( ( int ` J ) ` S ) = (/) ) ) -> ( X =/= (/) -> ( X \ S ) =/= (/) ) )
16 15 imp 
 |-  ( ( ( J e. Top /\ ( S C_ X /\ ( ( int ` J ) ` S ) = (/) ) ) /\ X =/= (/) ) -> ( X \ S ) =/= (/) )
17 16 an32s 
 |-  ( ( ( J e. Top /\ X =/= (/) ) /\ ( S C_ X /\ ( ( int ` J ) ` S ) = (/) ) ) -> ( X \ S ) =/= (/) )