Metamath Proof Explorer

Theorem mrcfval

Description: Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis mrcfval.f 
|- F = ( mrCls ` C )
Assertion mrcfval 
|- ( C e. ( Moore ` X ) -> F = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 fvssunirn 
 |-  ( Moore ` X ) C_ U. ran Moore
3 2 sseli 
 |-  ( C e. ( Moore ` X ) -> C e. U. ran Moore )
4 unieq 
 |-  ( c = C -> U. c = U. C )
5 4 pweqd 
 |-  ( c = C -> ~P U. c = ~P U. C )
6 rabeq 
 |-  ( c = C -> { s e. c | x C_ s } = { s e. C | x C_ s } )
7 6 inteqd 
 |-  ( c = C -> |^| { s e. c | x C_ s } = |^| { s e. C | x C_ s } )
8 5 7 mpteq12dv 
 |-  ( c = C -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) = ( x e. ~P U. C |-> |^| { s e. C | x C_ s } ) )
9 df-mrc 
 |-  mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )
10 mreunirn 
 |-  ( c e. U. ran Moore <-> c e. ( Moore ` U. c ) )
11 mrcflem 
 |-  ( c e. ( Moore ` U. c ) -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) : ~P U. c --> c )
12 10 11 sylbi 
 |-  ( c e. U. ran Moore -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) : ~P U. c --> c )
13 fssxp 
 |-  ( ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) : ~P U. c --> c -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) C_ ( ~P U. c X. c ) )
14 12 13 syl 
 |-  ( c e. U. ran Moore -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) C_ ( ~P U. c X. c ) )
15 vuniex 
 |-  U. c e. _V
16 15 pwex 
 |-  ~P U. c e. _V
17 vex 
 |-  c e. _V
18 16 17 xpex 
 |-  ( ~P U. c X. c ) e. _V
19 ssexg 
 |-  ( ( ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) C_ ( ~P U. c X. c ) /\ ( ~P U. c X. c ) e. _V ) -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) e. _V )
20 14 18 19 sylancl 
 |-  ( c e. U. ran Moore -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) e. _V )
21 8 9 20 fvmpt3 
 |-  ( C e. U. ran Moore -> ( mrCls ` C ) = ( x e. ~P U. C |-> |^| { s e. C | x C_ s } ) )
22 3 21 syl 
 |-  ( C e. ( Moore ` X ) -> ( mrCls ` C ) = ( x e. ~P U. C |-> |^| { s e. C | x C_ s } ) )
23 mreuni 
 |-  ( C e. ( Moore ` X ) -> U. C = X )
24 23 pweqd 
 |-  ( C e. ( Moore ` X ) -> ~P U. C = ~P X )
25 24 mpteq1d 
 |-  ( C e. ( Moore ` X ) -> ( x e. ~P U. C |-> |^| { s e. C | x C_ s } ) = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )
26 22 25 eqtrd 
 |-  ( C e. ( Moore ` X ) -> ( mrCls ` C ) = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )
27 1 26 syl5eq 
 |-  ( C e. ( Moore ` X ) -> F = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )