Metamath Proof Explorer

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 = J
Assertion cldopn S Clsd J X S J


Step Hyp Ref Expression
1 iscld.1 X = J
2 cldrcl S Clsd J J Top
3 1 iscld J Top S Clsd J S X X S J
4 3 simplbda J Top S Clsd J X S J
5 2 4 mpancom S Clsd J X S J