This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isopn2

Description: A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006)

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

Proof

Step Hyp Ref Expression
1 iscld.1 
 |-  X = U. J
2 difss 
 |-  ( X \ S ) C_ X
3 1 iscld2 
 |-  ( ( J e. Top /\ ( X \ S ) C_ X ) -> ( ( X \ S ) e. ( Clsd ` J ) <-> ( X \ ( X \ S ) ) e. J ) )
4 2 3 mpan2 
 |-  ( J e. Top -> ( ( X \ S ) e. ( Clsd ` J ) <-> ( X \ ( X \ S ) ) e. J ) )
5 dfss4 
 |-  ( S C_ X <-> ( X \ ( X \ S ) ) = S )
6 5 biimpi 
 |-  ( S C_ X -> ( X \ ( X \ S ) ) = S )
7 6 eleq1d 
 |-  ( S C_ X -> ( ( X \ ( X \ S ) ) e. J <-> S e. J ) )
8 4 7 sylan9bb 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( X \ S ) e. ( Clsd ` J ) <-> S e. J ) )
9 8 bicomd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( X \ S ) e. ( Clsd ` J ) ) )