Metamath Proof Explorer

Theorem difelcarsg

Description: The Caratheodory measurable sets are closed under complement. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
difelcarsg.1 
|- ( ph -> A e. ( toCaraSiga ` M ) )
Assertion difelcarsg 
|- ( ph -> ( O \ 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 difelcarsg.1 
 |-  ( ph -> A e. ( toCaraSiga ` M ) )
4 difssd 
 |-  ( ph -> ( O \ A ) C_ O )
5 indif2 
 |-  ( e i^i ( O \ A ) ) = ( ( e i^i O ) \ A )
6 elpwi 
 |-  ( e e. ~P O -> e C_ O )
7 6 adantl 
 |-  ( ( ph /\ e e. ~P O ) -> e C_ O )
8 dfss2 
 |-  ( e C_ O <-> ( e i^i O ) = e )
9 7 8 sylib 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i O ) = e )
10 9 difeq1d 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( e i^i O ) \ A ) = ( e \ A ) )
11 5 10 eqtrid 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i ( O \ A ) ) = ( e \ A ) )
12 11 fveq2d 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i ( O \ A ) ) ) = ( M ` ( e \ A ) ) )
13 difdif2 
 |-  ( e \ ( O \ A ) ) = ( ( e \ O ) u. ( e i^i A ) )
14 ssdif0 
 |-  ( e C_ O <-> ( e \ O ) = (/) )
15 7 14 sylib 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ O ) = (/) )
16 15 uneq1d 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( e \ O ) u. ( e i^i A ) ) = ( (/) u. ( e i^i A ) ) )
17 uncom 
 |-  ( ( e i^i A ) u. (/) ) = ( (/) u. ( e i^i A ) )
18 un0 
 |-  ( ( e i^i A ) u. (/) ) = ( e i^i A )
19 17 18 eqtr3i 
 |-  ( (/) u. ( e i^i A ) ) = ( e i^i A )
20 16 19 eqtrdi 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( e \ O ) u. ( e i^i A ) ) = ( e i^i A ) )
21 13 20 eqtrid 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ ( O \ A ) ) = ( e i^i A ) )
22 21 fveq2d 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ ( O \ A ) ) ) = ( M ` ( e i^i A ) ) )
23 12 22 oveq12d 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( O \ A ) ) ) +e ( M ` ( e \ ( O \ A ) ) ) ) = ( ( M ` ( e \ A ) ) +e ( M ` ( e i^i A ) ) ) )
24 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
25 2 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> M : ~P O --> ( 0 [,] +oo ) )
26 simpr 
 |-  ( ( ph /\ e e. ~P O ) -> e e. ~P O )
27 26 elpwdifcl 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ A ) e. ~P O )
28 25 27 ffvelcdmd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ A ) ) e. ( 0 [,] +oo ) )
29 24 28 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ A ) ) e. RR* )
30 26 elpwincl1 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i A ) e. ~P O )
31 25 30 ffvelcdmd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i A ) ) e. ( 0 [,] +oo ) )
32 24 31 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i A ) ) e. RR* )
33 xaddcom 
 |-  ( ( ( M ` ( e \ A ) ) e. RR* /\ ( M ` ( e i^i A ) ) e. RR* ) -> ( ( M ` ( e \ A ) ) +e ( M ` ( e i^i A ) ) ) = ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) )
34 29 32 33 syl2anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e \ A ) ) +e ( M ` ( e i^i A ) ) ) = ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) )
35 1 2 elcarsg 
 |-  ( ph -> ( A e. ( toCaraSiga ` M ) <-> ( A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) ) ) )
36 3 35 mpbid 
 |-  ( ph -> ( A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) ) )
37 36 simprd 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) )
38 37 r19.21bi 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) )
39 23 34 38 3eqtrd 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( O \ A ) ) ) +e ( M ` ( e \ ( O \ A ) ) ) ) = ( M ` e ) )
40 39 ralrimiva 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i ( O \ A ) ) ) +e ( M ` ( e \ ( O \ A ) ) ) ) = ( M ` e ) )
41 4 40 jca 
 |-  ( ph -> ( ( O \ A ) C_ O /\ A. e e. ~P O ( ( M ` ( e i^i ( O \ A ) ) ) +e ( M ` ( e \ ( O \ A ) ) ) ) = ( M ` e ) ) )
42 1 2 elcarsg 
 |-  ( ph -> ( ( O \ A ) e. ( toCaraSiga ` M ) <-> ( ( O \ A ) C_ O /\ A. e e. ~P O ( ( M ` ( e i^i ( O \ A ) ) ) +e ( M ` ( e \ ( O \ A ) ) ) ) = ( M ` e ) ) ) )
43 41 42 mpbird 
 |-  ( ph -> ( O \ A ) e. ( toCaraSiga ` M ) )