Metamath Proof Explorer

Theorem caragenunidm

Description: The base set of an outer measure belongs to the sigma-algebra generated by the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragenunidm.o 
|- ( ph -> O e. OutMeas )
caragenunidm.x 
|- X = U. dom O
caragenunidm.s 
|- S = ( CaraGen ` O )
Assertion caragenunidm 
|- ( ph -> X e. S )

Proof

Step Hyp Ref Expression
1 caragenunidm.o 
 |-  ( ph -> O e. OutMeas )
2 caragenunidm.x 
 |-  X = U. dom O
3 caragenunidm.s 
 |-  S = ( CaraGen ` O )
4 dmexg 
 |-  ( O e. OutMeas -> dom O e. _V )
5 uniexg 
 |-  ( dom O e. _V -> U. dom O e. _V )
6 1 4 5 3syl 
 |-  ( ph -> U. dom O e. _V )
7 2 6 eqeltrid 
 |-  ( ph -> X e. _V )
8 pwidg 
 |-  ( X e. _V -> X e. ~P X )
9 7 8 syl 
 |-  ( ph -> X e. ~P X )
10 elpwi 
 |-  ( a e. ~P X -> a C_ X )
11 dfss2 
 |-  ( a C_ X <-> ( a i^i X ) = a )
12 11 biimpi 
 |-  ( a C_ X -> ( a i^i X ) = a )
13 10 12 syl 
 |-  ( a e. ~P X -> ( a i^i X ) = a )
14 13 fveq2d 
 |-  ( a e. ~P X -> ( O ` ( a i^i X ) ) = ( O ` a ) )
15 14 adantl 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` ( a i^i X ) ) = ( O ` a ) )
16 ssdif0 
 |-  ( a C_ X <-> ( a \ X ) = (/) )
17 10 16 sylib 
 |-  ( a e. ~P X -> ( a \ X ) = (/) )
18 17 fveq2d 
 |-  ( a e. ~P X -> ( O ` ( a \ X ) ) = ( O ` (/) ) )
19 18 adantl 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` ( a \ X ) ) = ( O ` (/) ) )
20 1 ome0 
 |-  ( ph -> ( O ` (/) ) = 0 )
21 20 adantr 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` (/) ) = 0 )
22 19 21 eqtrd 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` ( a \ X ) ) = 0 )
23 15 22 oveq12d 
 |-  ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i X ) ) +e ( O ` ( a \ X ) ) ) = ( ( O ` a ) +e 0 ) )
24 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
25 1 adantr 
 |-  ( ( ph /\ a e. ~P X ) -> O e. OutMeas )
26 10 adantl 
 |-  ( ( ph /\ a e. ~P X ) -> a C_ X )
27 25 2 26 omecl 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` a ) e. ( 0 [,] +oo ) )
28 24 27 sselid 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` a ) e. RR* )
29 28 xaddridd 
 |-  ( ( ph /\ a e. ~P X ) -> ( ( O ` a ) +e 0 ) = ( O ` a ) )
30 eqidd 
 |-  ( ( ph /\ a e. ~P X ) -> ( O ` a ) = ( O ` a ) )
31 23 29 30 3eqtrd 
 |-  ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i X ) ) +e ( O ` ( a \ X ) ) ) = ( O ` a ) )
32 1 2 3 9 31 carageneld 
 |-  ( ph -> X e. S )