Metamath Proof Explorer


Theorem opncld

Description: The complement of an open set is closed. (Contributed by NM, 6-Oct-2006)

Ref Expression
Hypothesis iscld.1
|- X = U. J
Assertion opncld
|- ( ( J e. Top /\ S e. J ) -> ( X \ S ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 iscld.1
 |-  X = U. J
2 simpr
 |-  ( ( J e. Top /\ S e. J ) -> S e. J )
3 1 eltopss
 |-  ( ( J e. Top /\ S e. J ) -> S C_ X )
4 1 isopn2
 |-  ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( X \ S ) e. ( Clsd ` J ) ) )
5 3 4 syldan
 |-  ( ( J e. Top /\ S e. J ) -> ( S e. J <-> ( X \ S ) e. ( Clsd ` J ) ) )
6 2 5 mpbid
 |-  ( ( J e. Top /\ S e. J ) -> ( X \ S ) e. ( Clsd ` J ) )