Metamath Proof Explorer


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 } )