Metamath Proof Explorer

Theorem carsgsiga

Description: The Caratheodory measurable sets constructed from outer measures form a Sigma-algebra. Statement (iii) of Theorem 1.11.4 of Bogachev p. 42. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
carsgsiga.1 
|- ( ph -> ( M ` (/) ) = 0 )
carsgsiga.2 
|- ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
carsgsiga.3 
|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
Assertion carsgsiga 
|- ( ph -> ( toCaraSiga ` M ) e. ( sigAlgebra ` O ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 
 |-  ( ph -> O e. V )
2 carsgval.2 
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 carsgsiga.1 
 |-  ( ph -> ( M ` (/) ) = 0 )
4 carsgsiga.2 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
5 carsgsiga.3 
 |-  ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
6 1 2 carsgcl 
 |-  ( ph -> ( toCaraSiga ` M ) C_ ~P O )
7 1 2 3 baselcarsg 
 |-  ( ph -> O e. ( toCaraSiga ` M ) )
8 1 adantr 
 |-  ( ( ph /\ g e. ( toCaraSiga ` M ) ) -> O e. V )
9 2 adantr 
 |-  ( ( ph /\ g e. ( toCaraSiga ` M ) ) -> M : ~P O --> ( 0 [,] +oo ) )
10 simpr 
 |-  ( ( ph /\ g e. ( toCaraSiga ` M ) ) -> g e. ( toCaraSiga ` M ) )
11 8 9 10 difelcarsg 
 |-  ( ( ph /\ g e. ( toCaraSiga ` M ) ) -> ( O \ g ) e. ( toCaraSiga ` M ) )
12 11 ralrimiva 
 |-  ( ph -> A. g e. ( toCaraSiga ` M ) ( O \ g ) e. ( toCaraSiga ` M ) )
13 1 ad2antrr 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) -> O e. V )
14 2 ad2antrr 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) -> M : ~P O --> ( 0 [,] +oo ) )
15 3 ad2antrr 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) -> ( M ` (/) ) = 0 )
16 4 3adant1r 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
17 16 3adant1r 
 |-  ( ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
18 5 3adant1r 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
19 18 3adant1r 
 |-  ( ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
20 simpr 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) -> g ~<_ _om )
21 elpwi 
 |-  ( g e. ~P ( toCaraSiga ` M ) -> g C_ ( toCaraSiga ` M ) )
22 21 ad2antlr 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) -> g C_ ( toCaraSiga ` M ) )
23 13 14 15 17 19 20 22 carsgclctun 
 |-  ( ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) /\ g ~<_ _om ) -> U. g e. ( toCaraSiga ` M ) )
24 23 ex 
 |-  ( ( ph /\ g e. ~P ( toCaraSiga ` M ) ) -> ( g ~<_ _om -> U. g e. ( toCaraSiga ` M ) ) )
25 24 ralrimiva 
 |-  ( ph -> A. g e. ~P ( toCaraSiga ` M ) ( g ~<_ _om -> U. g e. ( toCaraSiga ` M ) ) )
26 7 12 25 3jca 
 |-  ( ph -> ( O e. ( toCaraSiga ` M ) /\ A. g e. ( toCaraSiga ` M ) ( O \ g ) e. ( toCaraSiga ` M ) /\ A. g e. ~P ( toCaraSiga ` M ) ( g ~<_ _om -> U. g e. ( toCaraSiga ` M ) ) ) )
27 6 26 jca 
 |-  ( ph -> ( ( toCaraSiga ` M ) C_ ~P O /\ ( O e. ( toCaraSiga ` M ) /\ A. g e. ( toCaraSiga ` M ) ( O \ g ) e. ( toCaraSiga ` M ) /\ A. g e. ~P ( toCaraSiga ` M ) ( g ~<_ _om -> U. g e. ( toCaraSiga ` M ) ) ) ) )
28 fvex 
 |-  ( toCaraSiga ` M ) e. _V
29 issiga 
 |-  ( ( toCaraSiga ` M ) e. _V -> ( ( toCaraSiga ` M ) e. ( sigAlgebra ` O ) <-> ( ( toCaraSiga ` M ) C_ ~P O /\ ( O e. ( toCaraSiga ` M ) /\ A. g e. ( toCaraSiga ` M ) ( O \ g ) e. ( toCaraSiga ` M ) /\ A. g e. ~P ( toCaraSiga ` M ) ( g ~<_ _om -> U. g e. ( toCaraSiga ` M ) ) ) ) ) )
30 28 29 ax-mp 
 |-  ( ( toCaraSiga ` M ) e. ( sigAlgebra ` O ) <-> ( ( toCaraSiga ` M ) C_ ~P O /\ ( O e. ( toCaraSiga ` M ) /\ A. g e. ( toCaraSiga ` M ) ( O \ g ) e. ( toCaraSiga ` M ) /\ A. g e. ~P ( toCaraSiga ` M ) ( g ~<_ _om -> U. g e. ( toCaraSiga ` M ) ) ) ) )
31 27 30 sylibr 
 |-  ( ph -> ( toCaraSiga ` M ) e. ( sigAlgebra ` O ) )