Theorem mrcidmd

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

	Ref	Expression
Hypotheses	mrcssidd.1	|- ( ph -> A e. ( Moore ` X ) )
	mrcssidd.2	|- N = ( mrCls ` A )
	mrcssidd.3	|- ( ph -> U C_ X )
Assertion	mrcidmd	|- ( ph -> ( N ` ( N ` U ) ) = ( N ` U ) )

Proof

Step	Hyp	Ref	Expression
1		mrcssidd.1	|- ( ph -> A e. ( Moore ` X ) )
2		mrcssidd.2	|- N = ( mrCls ` A )
3		mrcssidd.3	|- ( ph -> U C_ X )
4	2	mrcidm	|- ( ( A e. ( Moore ` X ) /\ U C_ X ) -> ( N ` ( N ` U ) ) = ( N ` U ) )
5	1 3 4	syl2anc	|- ( ph -> ( N ` ( N ` U ) ) = ( N ` U ) )