Metamath Proof Explorer

Theorem 0cld

Description: The empty set is closed. Part of Theorem 6.1(1) of Munkres p. 93. (Contributed by NM, 4-Oct-2006)

Ref Expression
Assertion 0cld 
|- ( J e. Top -> (/) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 dif0 
 |-  ( U. J \ (/) ) = U. J
2 1 topopn 
 |-  ( J e. Top -> ( U. J \ (/) ) e. J )
3 0ss 
 |-  (/) C_ U. J
4 eqid 
 |-  U. J = U. J
5 4 iscld2 
 |-  ( ( J e. Top /\ (/) C_ U. J ) -> ( (/) e. ( Clsd ` J ) <-> ( U. J \ (/) ) e. J ) )
6 3 5 mpan2 
 |-  ( J e. Top -> ( (/) e. ( Clsd ` J ) <-> ( U. J \ (/) ) e. J ) )
7 2 6 mpbird 
 |-  ( J e. Top -> (/) e. ( Clsd ` J ) )