Metamath Proof Explorer

Theorem cldss

Description: A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypothesis iscld.1 X = J
Assertion cldss S Clsd J S X


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 simprbda J Top S Clsd J S X
5 2 4 mpancom S Clsd J S X