Theorem mrcval

Description: Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Fan Zheng, 6-Jun-2016)

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2	1	mrcfval	|- ( C e. ( Moore ` X ) -> F = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )
3	2	adantr	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> F = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )
4		sseq1	|- ( x = U -> ( x C_ s <-> U C_ s ) )
5	4	rabbidv	|- ( x = U -> { s e. C | x C_ s } = { s e. C | U C_ s } )
6	5	inteqd	|- ( x = U -> |^| { s e. C | x C_ s } = |^| { s e. C | U C_ s } )
7	6	adantl	|- ( ( ( C e. ( Moore ` X ) /\ U C_ X ) /\ x = U ) -> |^| { s e. C | x C_ s } = |^| { s e. C | U C_ s } )
8		mre1cl	|- ( C e. ( Moore ` X ) -> X e. C )
9		elpw2g	|- ( X e. C -> ( U e. ~P X <-> U C_ X ) )
10	8 9	syl	|- ( C e. ( Moore ` X ) -> ( U e. ~P X <-> U C_ X ) )
11	10	biimpar	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U e. ~P X )
12		sseq2	|- ( s = X -> ( U C_ s <-> U C_ X ) )
13	8	adantr	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> X e. C )
14		simpr	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U C_ X )
15	12 13 14	elrabd	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> X e. { s e. C | U C_ s } )
16	15	ne0d	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> { s e. C | U C_ s } =/= (/) )
17		intex	|- ( { s e. C | U C_ s } =/= (/) <-> |^| { s e. C | U C_ s } e. _V )
18	16 17	sylib	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> |^| { s e. C | U C_ s } e. _V )
19	3 7 11 18	fvmptd	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )