Metamath Proof Explorer

Theorem clduni

Description: The union of closed sets is the underlying set of the topology (the union of open sets). (Contributed by Zhi Wang, 6-Sep-2024)

Ref Expression
Assertion clduni 
|- ( J e. Top -> U. ( Clsd ` J ) = U. J )

Proof

Step Hyp Ref Expression
1 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
2 1 biimpi 
 |-  ( J e. Top -> J e. ( TopOn ` U. J ) )
3 cldmreon 
 |-  ( J e. ( TopOn ` U. J ) -> ( Clsd ` J ) e. ( Moore ` U. J ) )
4 mreuni 
 |-  ( ( Clsd ` J ) e. ( Moore ` U. J ) -> U. ( Clsd ` J ) = U. J )
5 2 3 4 3syl 
 |-  ( J e. Top -> U. ( Clsd ` J ) = U. J )