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 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
mrcssidd.2 𝑁 = ( mrCls ‘ 𝐴 )
mrcssidd.3 ( 𝜑𝑈𝑋 )
Assertion mrcidmd ( 𝜑 → ( 𝑁 ‘ ( 𝑁𝑈 ) ) = ( 𝑁𝑈 ) )

Proof

Step Hyp Ref Expression
1 mrcssidd.1 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mrcssidd.2 𝑁 = ( mrCls ‘ 𝐴 )
3 mrcssidd.3 ( 𝜑𝑈𝑋 )
4 2 mrcidm ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝑋 ) → ( 𝑁 ‘ ( 𝑁𝑈 ) ) = ( 𝑁𝑈 ) )
5 1 3 4 syl2anc ( 𝜑 → ( 𝑁 ‘ ( 𝑁𝑈 ) ) = ( 𝑁𝑈 ) )