Metamath Proof Explorer

Theorem carsgclctun

Description: The Caratheodory measurable sets are closed under countable union. (Contributed by Thierry Arnoux, 21-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 ) )
carsgclctun.1 
|- ( ph -> A ~<_ _om )
carsgclctun.2 
|- ( ph -> A C_ ( toCaraSiga ` M ) )
Assertion carsgclctun 
|- ( ph -> U. A e. ( toCaraSiga ` M ) )

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 carsgclctun.1 
 |-  ( ph -> A ~<_ _om )
7 carsgclctun.2 
 |-  ( ph -> A C_ ( toCaraSiga ` M ) )
8 7 unissd 
 |-  ( ph -> U. A C_ U. ( toCaraSiga ` M ) )
9 1 2 3 carsguni 
 |-  ( ph -> U. ( toCaraSiga ` M ) = O )
10 8 9 sseqtrd 
 |-  ( ph -> U. A C_ O )
11 1 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> O e. V )
12 2 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> M : ~P O --> ( 0 [,] +oo ) )
13 3 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` (/) ) = 0 )
14 4 3adant1r 
 |-  ( ( ( ph /\ e e. ~P O ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
15 5 3adant1r 
 |-  ( ( ( ph /\ e e. ~P O ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
16 6 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> A ~<_ _om )
17 7 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> A C_ ( toCaraSiga ` M ) )
18 simpr 
 |-  ( ( ph /\ e e. ~P O ) -> e e. ~P O )
19 11 12 13 14 15 16 17 18 carsgclctunlem3 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) <_ ( M ` e ) )
20 inex1g 
 |-  ( e e. ~P O -> ( e i^i U. A ) e. _V )
21 20 adantl 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i U. A ) e. _V )
22 difexg 
 |-  ( e e. ~P O -> ( e \ U. A ) e. _V )
23 22 adantl 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ U. A ) e. _V )
24 prct 
 |-  ( ( ( e i^i U. A ) e. _V /\ ( e \ U. A ) e. _V ) -> { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om )
25 21 23 24 syl2anc 
 |-  ( ( ph /\ e e. ~P O ) -> { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om )
26 18 elpwincl1 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i U. A ) e. ~P O )
27 18 elpwdifcl 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ U. A ) e. ~P O )
28 prssi 
 |-  ( ( ( e i^i U. A ) e. ~P O /\ ( e \ U. A ) e. ~P O ) -> { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O )
29 26 27 28 syl2anc 
 |-  ( ( ph /\ e e. ~P O ) -> { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O )
30 prex 
 |-  { ( e i^i U. A ) , ( e \ U. A ) } e. _V
31 breq1 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> ( x ~<_ _om <-> { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om ) )
32 sseq1 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> ( x C_ ~P O <-> { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O ) )
33 31 32 3anbi23d 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) <-> ( ph /\ { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om /\ { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O ) ) )
34 unieq 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> U. x = U. { ( e i^i U. A ) , ( e \ U. A ) } )
35 34 fveq2d 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> ( M ` U. x ) = ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) )
36 esumeq1 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> sum* y e. x ( M ` y ) = sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) )
37 35 36 breq12d 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> ( ( M ` U. x ) <_ sum* y e. x ( M ` y ) <-> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) <_ sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) ) )
38 33 37 imbi12d 
 |-  ( x = { ( e i^i U. A ) , ( e \ U. A ) } -> ( ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) ) <-> ( ( ph /\ { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om /\ { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O ) -> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) <_ sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) ) ) )
39 38 4 vtoclg 
 |-  ( { ( e i^i U. A ) , ( e \ U. A ) } e. _V -> ( ( ph /\ { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om /\ { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O ) -> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) <_ sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) ) )
40 30 39 ax-mp 
 |-  ( ( ph /\ { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om /\ { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O ) -> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) <_ sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) )
41 40 3adant1r 
 |-  ( ( ( ph /\ e e. ~P O ) /\ { ( e i^i U. A ) , ( e \ U. A ) } ~<_ _om /\ { ( e i^i U. A ) , ( e \ U. A ) } C_ ~P O ) -> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) <_ sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) )
42 25 29 41 mpd3an23 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) <_ sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) )
43 uniprg 
 |-  ( ( ( e i^i U. A ) e. ~P O /\ ( e \ U. A ) e. ~P O ) -> U. { ( e i^i U. A ) , ( e \ U. A ) } = ( ( e i^i U. A ) u. ( e \ U. A ) ) )
44 26 27 43 syl2anc 
 |-  ( ( ph /\ e e. ~P O ) -> U. { ( e i^i U. A ) , ( e \ U. A ) } = ( ( e i^i U. A ) u. ( e \ U. A ) ) )
45 inundif 
 |-  ( ( e i^i U. A ) u. ( e \ U. A ) ) = e
46 44 45 eqtrdi 
 |-  ( ( ph /\ e e. ~P O ) -> U. { ( e i^i U. A ) , ( e \ U. A ) } = e )
47 46 fveq2d 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` U. { ( e i^i U. A ) , ( e \ U. A ) } ) = ( M ` e ) )
48 simpr 
 |-  ( ( ( ph /\ e e. ~P O ) /\ y = ( e i^i U. A ) ) -> y = ( e i^i U. A ) )
49 48 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O ) /\ y = ( e i^i U. A ) ) -> ( M ` y ) = ( M ` ( e i^i U. A ) ) )
50 simpr 
 |-  ( ( ( ph /\ e e. ~P O ) /\ y = ( e \ U. A ) ) -> y = ( e \ U. A ) )
51 50 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O ) /\ y = ( e \ U. A ) ) -> ( M ` y ) = ( M ` ( e \ U. A ) ) )
52 12 26 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i U. A ) ) e. ( 0 [,] +oo ) )
53 12 27 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ U. A ) ) e. ( 0 [,] +oo ) )
54 ineq2 
 |-  ( ( e i^i U. A ) = ( e \ U. A ) -> ( ( e i^i U. A ) i^i ( e i^i U. A ) ) = ( ( e i^i U. A ) i^i ( e \ U. A ) ) )
55 inidm 
 |-  ( ( e i^i U. A ) i^i ( e i^i U. A ) ) = ( e i^i U. A )
56 inindif 
 |-  ( ( e i^i U. A ) i^i ( e \ U. A ) ) = (/)
57 54 55 56 3eqtr3g 
 |-  ( ( e i^i U. A ) = ( e \ U. A ) -> ( e i^i U. A ) = (/) )
58 57 adantl 
 |-  ( ( ( ph /\ e e. ~P O ) /\ ( e i^i U. A ) = ( e \ U. A ) ) -> ( e i^i U. A ) = (/) )
59 58 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O ) /\ ( e i^i U. A ) = ( e \ U. A ) ) -> ( M ` ( e i^i U. A ) ) = ( M ` (/) ) )
60 3 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P O ) /\ ( e i^i U. A ) = ( e \ U. A ) ) -> ( M ` (/) ) = 0 )
61 59 60 eqtrd 
 |-  ( ( ( ph /\ e e. ~P O ) /\ ( e i^i U. A ) = ( e \ U. A ) ) -> ( M ` ( e i^i U. A ) ) = 0 )
62 61 orcd 
 |-  ( ( ( ph /\ e e. ~P O ) /\ ( e i^i U. A ) = ( e \ U. A ) ) -> ( ( M ` ( e i^i U. A ) ) = 0 \/ ( M ` ( e i^i U. A ) ) = +oo ) )
63 62 ex 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( e i^i U. A ) = ( e \ U. A ) -> ( ( M ` ( e i^i U. A ) ) = 0 \/ ( M ` ( e i^i U. A ) ) = +oo ) ) )
64 49 51 26 27 52 53 63 esumpr2 
 |-  ( ( ph /\ e e. ~P O ) -> sum* y e. { ( e i^i U. A ) , ( e \ U. A ) } ( M ` y ) = ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) )
65 42 47 64 3brtr3d 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) <_ ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) )
66 19 65 jca 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) <_ ( M ` e ) /\ ( M ` e ) <_ ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) ) )
67 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
68 67 52 sseldi 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i U. A ) ) e. RR* )
69 67 53 sseldi 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ U. A ) ) e. RR* )
70 68 69 xaddcld 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) e. RR* )
71 2 ffvelrnda 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) )
72 67 71 sseldi 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. RR* )
73 xrletri3 
 |-  ( ( ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) e. RR* /\ ( M ` e ) e. RR* ) -> ( ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) = ( M ` e ) <-> ( ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) <_ ( M ` e ) /\ ( M ` e ) <_ ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) ) ) )
74 70 72 73 syl2anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) = ( M ` e ) <-> ( ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) <_ ( M ` e ) /\ ( M ` e ) <_ ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) ) ) )
75 66 74 mpbird 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) = ( M ` e ) )
76 75 ralrimiva 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) = ( M ` e ) )
77 1 2 elcarsg 
 |-  ( ph -> ( U. A e. ( toCaraSiga ` M ) <-> ( U. A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U. A ) ) +e ( M ` ( e \ U. A ) ) ) = ( M ` e ) ) ) )
78 10 76 77 mpbir2and 
 |-  ( ph -> U. A e. ( toCaraSiga ` M ) )