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 df-ss
 |-  ( 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 ffvelrnd
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) )
20 16 19 sselid
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. RR* )
21 xaddid1
 |-  ( ( 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 ) )