Metamath Proof Explorer


Theorem iscld4

Description: A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008)

Ref Expression
Hypothesis clscld.1 X = J
Assertion iscld4 J Top S X S Clsd J cls J S S

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 1 iscld3 J Top S X S Clsd J cls J S = S
3 eqss cls J S = S cls J S S S cls J S
4 1 sscls J Top S X S cls J S
5 4 biantrud J Top S X cls J S S cls J S S S cls J S
6 3 5 bitr4id J Top S X cls J S = S cls J S S
7 2 6 bitrd J Top S X S Clsd J cls J S S