Theorem mrccl

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

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2	1	mrcf	|- ( C e. ( Moore ` X ) -> F : ~P X --> C )
3	2	adantr	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> F : ~P X --> C )
4		mre1cl	|- ( C e. ( Moore ` X ) -> X e. C )
5		elpw2g	|- ( X e. C -> ( U e. ~P X <-> U C_ X ) )
6	4 5	syl	|- ( C e. ( Moore ` X ) -> ( U e. ~P X <-> U C_ X ) )
7	6	biimpar	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U e. ~P X )
8	3 7	ffvelcdmd	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) e. C )