Theorem cldopn

Description: The complement of a closed set is open. (Contributed by NM, 5-Oct-2006) (Revised by Stefan O'Rear, 22-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2		cldrcl	|- ( S e. ( Clsd ` J ) -> J e. Top )
3	1	iscld	|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
4	3	simplbda	|- ( ( J e. Top /\ S e. ( Clsd ` J ) ) -> ( X \ S ) e. J )
5	2 4	mpancom	|- ( S e. ( Clsd ` J ) -> ( X \ S ) e. J )