Theorem mrcf

Description: The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	|- F = ( mrCls ` C )
Assertion	mrcf	|- ( C e. ( Moore ` X ) -> F : ~P X --> C )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		mrcflem	|- ( C e. ( Moore ` X ) -> ( x e. ~P X |-> |^| { s e. C | x C_ s } ) : ~P X --> C )
3	1	mrcfval	|- ( C e. ( Moore ` X ) -> F = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )
4	3	feq1d	|- ( C e. ( Moore ` X ) -> ( F : ~P X --> C <-> ( x e. ~P X |-> |^| { s e. C | x C_ s } ) : ~P X --> C ) )
5	2 4	mpbird	|- ( C e. ( Moore ` X ) -> F : ~P X --> C )