Theorem mrcid

Description: The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	|- F = ( mrCls ` C )
Assertion	mrcid	|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = U )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		mress	|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> U C_ X )
3	1	mrcval	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
4	2 3	syldan	|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
5		intmin	|- ( U e. C -> |^| { s e. C | U C_ s } = U )
6	5	adantl	|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> |^| { s e. C | U C_ s } = U )
7	4 6	eqtrd	|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = U )