Metamath Proof Explorer

Theorem fiunelcarsg

Description: The Caratheodory measurable sets are closed under finite union. (Contributed by Thierry Arnoux, 23-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 ) )
fiunelcarsg.1 
|- ( ph -> A e. Fin )
fiunelcarsg.2 
|- ( ph -> A C_ ( toCaraSiga ` M ) )
Assertion fiunelcarsg 
|- ( 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 fiunelcarsg.1 
 |-  ( ph -> A e. Fin )
6 fiunelcarsg.2 
 |-  ( ph -> A C_ ( toCaraSiga ` M ) )
7 unieq 
 |-  ( a = (/) -> U. a = U. (/) )
8 eqidd 
 |-  ( a = (/) -> ( toCaraSiga ` M ) = ( toCaraSiga ` M ) )
9 7 8 eleq12d 
 |-  ( a = (/) -> ( U. a e. ( toCaraSiga ` M ) <-> U. (/) e. ( toCaraSiga ` M ) ) )
10 unieq 
 |-  ( a = b -> U. a = U. b )
11 eqidd 
 |-  ( a = b -> ( toCaraSiga ` M ) = ( toCaraSiga ` M ) )
12 10 11 eleq12d 
 |-  ( a = b -> ( U. a e. ( toCaraSiga ` M ) <-> U. b e. ( toCaraSiga ` M ) ) )
13 unieq 
 |-  ( a = ( b u. { x } ) -> U. a = U. ( b u. { x } ) )
14 eqidd 
 |-  ( a = ( b u. { x } ) -> ( toCaraSiga ` M ) = ( toCaraSiga ` M ) )
15 13 14 eleq12d 
 |-  ( a = ( b u. { x } ) -> ( U. a e. ( toCaraSiga ` M ) <-> U. ( b u. { x } ) e. ( toCaraSiga ` M ) ) )
16 unieq 
 |-  ( a = A -> U. a = U. A )
17 eqidd 
 |-  ( a = A -> ( toCaraSiga ` M ) = ( toCaraSiga ` M ) )
18 16 17 eleq12d 
 |-  ( a = A -> ( U. a e. ( toCaraSiga ` M ) <-> U. A e. ( toCaraSiga ` M ) ) )
19 uni0 
 |-  U. (/) = (/)
20 difid 
 |-  ( O \ O ) = (/)
21 19 20 eqtr4i 
 |-  U. (/) = ( O \ O )
22 1 2 3 baselcarsg 
 |-  ( ph -> O e. ( toCaraSiga ` M ) )
23 1 2 22 difelcarsg 
 |-  ( ph -> ( O \ O ) e. ( toCaraSiga ` M ) )
24 21 23 eqeltrid 
 |-  ( ph -> U. (/) e. ( toCaraSiga ` M ) )
25 uniun 
 |-  U. ( b u. { x } ) = ( U. b u. U. { x } )
26 vex 
 |-  x e. _V
27 26 unisn 
 |-  U. { x } = x
28 27 uneq2i 
 |-  ( U. b u. U. { x } ) = ( U. b u. x )
29 25 28 eqtri 
 |-  U. ( b u. { x } ) = ( U. b u. x )
30 1 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> O e. V )
31 2 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> M : ~P O --> ( 0 [,] +oo ) )
32 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> U. b e. ( toCaraSiga ` M ) )
33 simpll 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> ph )
34 1 2 3 4 carsgsigalem 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )
35 33 34 syl3an1 
 |-  ( ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) /\ e e. ~P O /\ f e. ~P O ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )
36 6 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> A C_ ( toCaraSiga ` M ) )
37 simplrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> x e. ( A \ b ) )
38 37 eldifad 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> x e. A )
39 36 38 sseldd 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> x e. ( toCaraSiga ` M ) )
40 30 31 32 35 39 unelcarsg 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> ( U. b u. x ) e. ( toCaraSiga ` M ) )
41 29 40 eqeltrid 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ U. b e. ( toCaraSiga ` M ) ) -> U. ( b u. { x } ) e. ( toCaraSiga ` M ) )
42 41 ex 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( U. b e. ( toCaraSiga ` M ) -> U. ( b u. { x } ) e. ( toCaraSiga ` M ) ) )
43 9 12 15 18 24 42 5 findcard2d 
 |-  ( ph -> U. A e. ( toCaraSiga ` M ) )