Metamath Proof Explorer

Theorem caragenval

Description: The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion caragenval 
|- ( O e. OutMeas -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( O e. OutMeas -> O e. OutMeas )
2 dmexg 
 |-  ( O e. OutMeas -> dom O e. _V )
3 2 uniexd 
 |-  ( O e. OutMeas -> U. dom O e. _V )
4 3 pwexd 
 |-  ( O e. OutMeas -> ~P U. dom O e. _V )
5 rabexg 
 |-  ( ~P U. dom O e. _V -> { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } e. _V )
6 4 5 syl 
 |-  ( O e. OutMeas -> { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } e. _V )
7 dmeq 
 |-  ( o = O -> dom o = dom O )
8 7 unieqd 
 |-  ( o = O -> U. dom o = U. dom O )
9 8 pweqd 
 |-  ( o = O -> ~P U. dom o = ~P U. dom O )
10 9 raleqdv 
 |-  ( o = O -> ( A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) <-> A. a e. ~P U. dom O ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) ) )
11 fveq1 
 |-  ( o = O -> ( o ` ( a i^i e ) ) = ( O ` ( a i^i e ) ) )
12 fveq1 
 |-  ( o = O -> ( o ` ( a \ e ) ) = ( O ` ( a \ e ) ) )
13 11 12 oveq12d 
 |-  ( o = O -> ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) )
14 fveq1 
 |-  ( o = O -> ( o ` a ) = ( O ` a ) )
15 13 14 eqeq12d 
 |-  ( o = O -> ( ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) <-> ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) ) )
16 15 ralbidv 
 |-  ( o = O -> ( A. a e. ~P U. dom O ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) <-> A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) ) )
17 10 16 bitrd 
 |-  ( o = O -> ( A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) <-> A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) ) )
18 9 17 rabeqbidv 
 |-  ( o = O -> { e e. ~P U. dom o | A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) } = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
19 df-caragen 
 |-  CaraGen = ( o e. OutMeas |-> { e e. ~P U. dom o | A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) } )
20 18 19 fvmptg 
 |-  ( ( O e. OutMeas /\ { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } e. _V ) -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
21 1 6 20 syl2anc 
 |-  ( O e. OutMeas -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )