Metamath Proof Explorer

Theorem 0nnei

Description: The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007)

Ref Expression
Assertion 0nnei 
|- ( ( J e. Top /\ S =/= (/) ) -> -. (/) e. ( ( nei ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 ssnei 
 |-  ( ( J e. Top /\ (/) e. ( ( nei ` J ) ` S ) ) -> S C_ (/) )
2 ss0b 
 |-  ( S C_ (/) <-> S = (/) )
3 1 2 sylib 
 |-  ( ( J e. Top /\ (/) e. ( ( nei ` J ) ` S ) ) -> S = (/) )
4 3 ex 
 |-  ( J e. Top -> ( (/) e. ( ( nei ` J ) ` S ) -> S = (/) ) )
5 4 necon3ad 
 |-  ( J e. Top -> ( S =/= (/) -> -. (/) e. ( ( nei ` J ) ` S ) ) )
6 5 imp 
 |-  ( ( J e. Top /\ S =/= (/) ) -> -. (/) e. ( ( nei ` J ) ` S ) )