This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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