Metamath Proof Explorer

Theorem 0elcarsg

Description: The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-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 0elcarsg 
|- ( ph -> (/) 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 0ss 
 |-  (/) C_ O
5 4 a1i 
 |-  ( ph -> (/) C_ O )
6 in0 
 |-  ( e i^i (/) ) = (/)
7 6 fveq2i 
 |-  ( M ` ( e i^i (/) ) ) = ( M ` (/) )
8 7 3 syl5eq 
 |-  ( ph -> ( M ` ( e i^i (/) ) ) = 0 )
9 dif0 
 |-  ( e \ (/) ) = e
10 9 fveq2i 
 |-  ( M ` ( e \ (/) ) ) = ( M ` e )
11 10 a1i 
 |-  ( ph -> ( M ` ( e \ (/) ) ) = ( M ` e ) )
12 8 11 oveq12d 
 |-  ( ph -> ( ( M ` ( e i^i (/) ) ) +e ( M ` ( e \ (/) ) ) ) = ( 0 +e ( M ` e ) ) )
13 12 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i (/) ) ) +e ( M ` ( e \ (/) ) ) ) = ( 0 +e ( M ` e ) ) )
14 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
15 2 ffvelrnda 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) )
16 14 15 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. RR* )
17 xaddid2 
 |-  ( ( M ` e ) e. RR* -> ( 0 +e ( M ` e ) ) = ( M ` e ) )
18 16 17 syl 
 |-  ( ( ph /\ e e. ~P O ) -> ( 0 +e ( M ` e ) ) = ( M ` e ) )
19 13 18 eqtrd 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i (/) ) ) +e ( M ` ( e \ (/) ) ) ) = ( M ` e ) )
20 19 ralrimiva 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i (/) ) ) +e ( M ` ( e \ (/) ) ) ) = ( M ` e ) )
21 1 2 elcarsg 
 |-  ( ph -> ( (/) e. ( toCaraSiga ` M ) <-> ( (/) C_ O /\ A. e e. ~P O ( ( M ` ( e i^i (/) ) ) +e ( M ` ( e \ (/) ) ) ) = ( M ` e ) ) ) )
22 5 20 21 mpbir2and 
 |-  ( ph -> (/) e. ( toCaraSiga ` M ) )