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

Metamath Proof Explorer

Theorem mrcidmd

Description: Moore closure is idempotent. Deduction form of mrcidm . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrcssidd.1 ⊢ φ → A ∈ Moore ⁡ X
mrcssidd.2 ⊢ N = mrCls ⁡ A
mrcssidd.3 ⊢ φ → U ⊆ X
Assertion mrcidmd ⊢ φ → N ⁡ N ⁡ U = N ⁡ U

Proof

Step Hyp Ref Expression
1 mrcssidd.1 ⊢ φ → A ∈ Moore ⁡ X
2 mrcssidd.2 ⊢ N = mrCls ⁡ A
3 mrcssidd.3 ⊢ φ → U ⊆ X
4 2 mrcidm ⊢ A ∈ Moore ⁡ X ∧ U ⊆ X → N ⁡ N ⁡ U = N ⁡ U
5 1 3 4 syl2anc ⊢ φ → N ⁡ N ⁡ U = N ⁡ U