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 ) ) |
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 ) ) |