Metamath Proof Explorer

Theorem cls0

Description: The closure of the empty set. (Contributed by NM, 2-Oct-2007) (Proof shortened by Jim Kingdon, 12-Mar-2023)

Ref Expression
Assertion cls0 
|- ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 0cld 
 |-  ( J e. Top -> (/) e. ( Clsd ` J ) )
2 cldcls 
 |-  ( (/) e. ( Clsd ` J ) -> ( ( cls ` J ) ` (/) ) = (/) )
3 1 2 syl 
 |-  ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )