Metamath Proof Explorer

Theorem carsgval

Description: Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
Assertion carsgval 
|- ( ph -> ( toCaraSiga ` M ) = { a e. ~P O | A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) } )

Proof

Step Hyp Ref Expression
1 carsgval.1 
 |-  ( ph -> O e. V )
2 carsgval.2 
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 df-carsg 
 |-  toCaraSiga = ( m e. _V |-> { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) } )
4 simpr 
 |-  ( ( ph /\ m = M ) -> m = M )
5 4 dmeqd 
 |-  ( ( ph /\ m = M ) -> dom m = dom M )
6 2 fdmd 
 |-  ( ph -> dom M = ~P O )
7 6 adantr 
 |-  ( ( ph /\ m = M ) -> dom M = ~P O )
8 5 7 eqtrd 
 |-  ( ( ph /\ m = M ) -> dom m = ~P O )
9 8 unieqd 
 |-  ( ( ph /\ m = M ) -> U. dom m = U. ~P O )
10 unipw 
 |-  U. ~P O = O
11 9 10 eqtrdi 
 |-  ( ( ph /\ m = M ) -> U. dom m = O )
12 11 pweqd 
 |-  ( ( ph /\ m = M ) -> ~P U. dom m = ~P O )
13 fveq1 
 |-  ( m = M -> ( m ` ( e i^i a ) ) = ( M ` ( e i^i a ) ) )
14 fveq1 
 |-  ( m = M -> ( m ` ( e \ a ) ) = ( M ` ( e \ a ) ) )
15 13 14 oveq12d 
 |-  ( m = M -> ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) )
16 fveq1 
 |-  ( m = M -> ( m ` e ) = ( M ` e ) )
17 15 16 eqeq12d 
 |-  ( m = M -> ( ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) <-> ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) ) )
18 17 adantl 
 |-  ( ( ph /\ m = M ) -> ( ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) <-> ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) ) )
19 12 18 raleqbidv 
 |-  ( ( ph /\ m = M ) -> ( A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) <-> A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) ) )
20 12 19 rabeqbidv 
 |-  ( ( ph /\ m = M ) -> { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) } = { a e. ~P O | A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) } )
21 1 pwexd 
 |-  ( ph -> ~P O e. _V )
22 2 21 fexd 
 |-  ( ph -> M e. _V )
23 pwexg 
 |-  ( O e. V -> ~P O e. _V )
24 rabexg 
 |-  ( ~P O e. _V -> { a e. ~P O | A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) } e. _V )
25 1 23 24 3syl 
 |-  ( ph -> { a e. ~P O | A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) } e. _V )
26 3 20 22 25 fvmptd2 
 |-  ( ph -> ( toCaraSiga ` M ) = { a e. ~P O | A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) } )