Metamath Proof Explorer

Definition df-carsg

Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval for its value. Definition 1.11.2 of Bogachev p. 41. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Assertion 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 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccarsg 
 |-  toCaraSiga
1 vm 
 |-  m
2 cvv 
 |-  _V
3 va 
 |-  a
4 1 cv 
 |-  m
5 4 cdm 
 |-  dom m
6 5 cuni 
 |-  U. dom m
7 6 cpw 
 |-  ~P U. dom m
8 ve 
 |-  e
9 8 cv 
 |-  e
10 3 cv 
 |-  a
11 9 10 cin 
 |-  ( e i^i a )
12 11 4 cfv 
 |-  ( m ` ( e i^i a ) )
13 cxad 
 |-  +e
14 9 10 cdif 
 |-  ( e \ a )
15 14 4 cfv 
 |-  ( m ` ( e \ a ) )
16 12 15 13 co 
 |-  ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) )
17 9 4 cfv 
 |-  ( m ` e )
18 16 17 wceq 
 |-  ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e )
19 18 8 7 wral 
 |-  A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e )
20 19 3 7 crab 
 |-  { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) }
21 1 2 20 cmpt 
 |-  ( 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 ) } )
22 0 21 wceq 
 |-  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 ) } )