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