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 e. ( Moore ` X ) /\ U C_ X ) -> ( F ` ( F ` U ) ) = ( F ` U ) )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2	1	mrccl	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) e. C )
3	1	mrcid	|- ( ( C e. ( Moore ` X ) /\ ( F ` U ) e. C ) -> ( F ` ( F ` U ) ) = ( F ` U ) )
4	2 3	syldan	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` ( F ` U ) ) = ( F ` U ) )