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 | ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ 𝑈 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mrcssidd.1 | ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) ) | |
2 | mrcssidd.2 | ⊢ 𝑁 = ( mrCls ‘ 𝐴 ) | |
3 | mrcssidd.3 | ⊢ ( 𝜑 → 𝑈 ⊆ 𝑋 ) | |
4 | 2 | mrcidm | ⊢ ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ 𝑈 ) ) |
5 | 1 3 4 | syl2anc | ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ 𝑈 ) ) |