Metamath Proof Explorer


Theorem carsgval

Description: Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 φOV
carsgval.2 φM:𝒫O0+∞
Assertion carsgval φtoCaraSigaM=a𝒫O|e𝒫OMea+𝑒Mea=Me

Proof

Step Hyp Ref Expression
1 carsgval.1 φOV
2 carsgval.2 φM:𝒫O0+∞
3 df-carsg toCaraSiga=mVa𝒫domm|e𝒫dommmea+𝑒mea=me
4 simpr φm=Mm=M
5 4 dmeqd φm=Mdomm=domM
6 2 fdmd φdomM=𝒫O
7 6 adantr φm=MdomM=𝒫O
8 5 7 eqtrd φm=Mdomm=𝒫O
9 8 unieqd φm=Mdomm=𝒫O
10 unipw 𝒫O=O
11 9 10 eqtrdi φm=Mdomm=O
12 11 pweqd φm=M𝒫domm=𝒫O
13 fveq1 m=Mmea=Mea
14 fveq1 m=Mmea=Mea
15 13 14 oveq12d m=Mmea+𝑒mea=Mea+𝑒Mea
16 fveq1 m=Mme=Me
17 15 16 eqeq12d m=Mmea+𝑒mea=meMea+𝑒Mea=Me
18 17 adantl φm=Mmea+𝑒mea=meMea+𝑒Mea=Me
19 12 18 raleqbidv φm=Me𝒫dommmea+𝑒mea=mee𝒫OMea+𝑒Mea=Me
20 12 19 rabeqbidv φm=Ma𝒫domm|e𝒫dommmea+𝑒mea=me=a𝒫O|e𝒫OMea+𝑒Mea=Me
21 1 pwexd φ𝒫OV
22 2 21 fexd φMV
23 pwexg OV𝒫OV
24 rabexg 𝒫OVa𝒫O|e𝒫OMea+𝑒Mea=MeV
25 1 23 24 3syl φa𝒫O|e𝒫OMea+𝑒Mea=MeV
26 3 20 22 25 fvmptd2 φtoCaraSigaM=a𝒫O|e𝒫OMea+𝑒Mea=Me