Database
BASIC STRUCTURES
Moore spaces
Moore closures
mrcidm
Next ⟩
mrcsscl
Metamath Proof Explorer
Ascii
Unicode
Theorem
mrcidm
Description:
The closure operation is idempotent.
(Contributed by
Stefan O'Rear
, 31-Jan-2015)
Ref
Expression
Hypothesis
mrcfval.f
⊢
F
=
mrCls
⁡
C
Assertion
mrcidm
⊢
C
∈
Moore
⁡
X
∧
U
⊆
X
→
F
⁡
F
⁡
U
=
F
⁡
U
Proof
Step
Hyp
Ref
Expression
1
mrcfval.f
⊢
F
=
mrCls
⁡
C
2
1
mrccl
⊢
C
∈
Moore
⁡
X
∧
U
⊆
X
→
F
⁡
U
∈
C
3
1
mrcid
⊢
C
∈
Moore
⁡
X
∧
F
⁡
U
∈
C
→
F
⁡
F
⁡
U
=
F
⁡
U
4
2
3
syldan
⊢
C
∈
Moore
⁡
X
∧
U
⊆
X
→
F
⁡
F
⁡
U
=
F
⁡
U