Metamath Proof Explorer

Theorem baselcarsg

Description: The universe set, O , is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
baselcarsg.1 
|- ( ph -> ( M ` (/) ) = 0 )
Assertion baselcarsg 
|- ( ph -> O 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 baselcarsg.1 
 |-  ( ph -> ( M ` (/) ) = 0 )
4 ssidd 
 |-  ( ph -> O C_ O )
5 elpwi 
 |-  ( e e. ~P O -> e C_ O )
6 5 adantl 
 |-  ( ( ph /\ e e. ~P O ) -> e C_ O )
7 dfss2 
 |-  ( e C_ O <-> ( e i^i O ) = e )
8 6 7 sylib 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i O ) = e )
9 8 fveq2d 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i O ) ) = ( M ` e ) )
10 ssdif0 
 |-  ( e C_ O <-> ( e \ O ) = (/) )
11 6 10 sylib 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ O ) = (/) )
12 11 fveq2d 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ O ) ) = ( M ` (/) ) )
13 3 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` (/) ) = 0 )
14 12 13 eqtrd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ O ) ) = 0 )
15 9 14 oveq12d 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( ( M ` e ) +e 0 ) )
16 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
17 2 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> M : ~P O --> ( 0 [,] +oo ) )
18 simpr 
 |-  ( ( ph /\ e e. ~P O ) -> e e. ~P O )
19 17 18 ffvelcdmd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) )
20 16 19 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. RR* )
21 xaddrid 
 |-  ( ( M ` e ) e. RR* -> ( ( M ` e ) +e 0 ) = ( M ` e ) )
22 20 21 syl 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` e ) +e 0 ) = ( M ` e ) )
23 15 22 eqtrd 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) )
24 23 ralrimiva 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) )
25 4 24 jca 
 |-  ( ph -> ( O C_ O /\ A. e e. ~P O ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) ) )
26 1 2 elcarsg 
 |-  ( ph -> ( O e. ( toCaraSiga ` M ) <-> ( O C_ O /\ A. e e. ~P O ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) ) ) )
27 25 26 mpbird 
 |-  ( ph -> O e. ( toCaraSiga ` M ) )