This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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