Database
BASIC TOPOLOGY
Topology
Closure and interior
iscld3
Next ⟩
iscld4
Metamath Proof Explorer
Ascii
Unicode
Theorem
iscld3
Description:
A subset is closed iff it equals its own closure.
(Contributed by
NM
, 2-Oct-2006)
Ref
Expression
Hypothesis
clscld.1
⊢
X
=
⋃
J
Assertion
iscld3
⊢
J
∈
Top
∧
S
⊆
X
→
S
∈
Clsd
⁡
J
↔
cls
⁡
J
⁡
S
=
S
Proof
Step
Hyp
Ref
Expression
1
clscld.1
⊢
X
=
⋃
J
2
cldcls
⊢
S
∈
Clsd
⁡
J
→
cls
⁡
J
⁡
S
=
S
3
1
clscld
⊢
J
∈
Top
∧
S
⊆
X
→
cls
⁡
J
⁡
S
∈
Clsd
⁡
J
4
eleq1
⊢
cls
⁡
J
⁡
S
=
S
→
cls
⁡
J
⁡
S
∈
Clsd
⁡
J
↔
S
∈
Clsd
⁡
J
5
3
4
syl5ibcom
⊢
J
∈
Top
∧
S
⊆
X
→
cls
⁡
J
⁡
S
=
S
→
S
∈
Clsd
⁡
J
6
2
5
impbid2
⊢
J
∈
Top
∧
S
⊆
X
→
S
∈
Clsd
⁡
J
↔
cls
⁡
J
⁡
S
=
S