Description: The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007) (Proof shortened by Jim Kingdon, 11-Mar-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | clscld.1 | |- X = U. J |
|
| Assertion | clstop | |- ( J e. Top -> ( ( cls ` J ) ` X ) = X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clscld.1 | |- X = U. J |
|
| 2 | 1 | topcld | |- ( J e. Top -> X e. ( Clsd ` J ) ) |
| 3 | cldcls | |- ( X e. ( Clsd ` J ) -> ( ( cls ` J ) ` X ) = X ) |
|
| 4 | 2 3 | syl | |- ( J e. Top -> ( ( cls ` J ) ` X ) = X ) |