Metamath Proof Explorer


Theorem inelcarsg

Description: The Caratheodory measurable sets are closed under intersection. (Contributed by Thierry Arnoux, 18-May-2020)

Ref Expression
Hypotheses carsgval.1 φOV
carsgval.2 φM:𝒫O0+∞
difelcarsg.1 φAtoCaraSigaM
inelcarsg.1 φa𝒫Ob𝒫OMabMa+𝑒Mb
inelcarsg.2 φBtoCaraSigaM
Assertion inelcarsg φABtoCaraSigaM

Proof

Step Hyp Ref Expression
1 carsgval.1 φOV
2 carsgval.2 φM:𝒫O0+∞
3 difelcarsg.1 φAtoCaraSigaM
4 inelcarsg.1 φa𝒫Ob𝒫OMabMa+𝑒Mb
5 inelcarsg.2 φBtoCaraSigaM
6 1 2 elcarsg φAtoCaraSigaMAOe𝒫OMeA+𝑒MeA=Me
7 3 6 mpbid φAOe𝒫OMeA+𝑒MeA=Me
8 7 simpld φAO
9 ssinss1 AOABO
10 8 9 syl φABO
11 iccssxr 0+∞*
12 2 adantr φe𝒫OM:𝒫O0+∞
13 simpr φe𝒫Oe𝒫O
14 13 elpwdifcl φe𝒫OeAB𝒫O
15 12 14 ffvelrnd φe𝒫OMeAB0+∞
16 11 15 sselid φe𝒫OMeAB*
17 13 elpwincl1 φe𝒫OeA𝒫O
18 17 elpwdifcl φe𝒫OeAB𝒫O
19 12 18 ffvelrnd φe𝒫OMeAB0+∞
20 11 19 sselid φe𝒫OMeAB*
21 13 elpwdifcl φe𝒫OeA𝒫O
22 12 21 ffvelrnd φe𝒫OMeA0+∞
23 11 22 sselid φe𝒫OMeA*
24 20 23 xaddcld φe𝒫OMeAB+𝑒MeA*
25 13 elpwincl1 φe𝒫OeAB𝒫O
26 12 25 ffvelrnd φe𝒫OMeAB0+∞
27 11 26 sselid φe𝒫OMeAB*
28 indifundif eABeA=eAB
29 28 fveq2i MeABeA=MeAB
30 4 3expb φa𝒫Ob𝒫OMabMa+𝑒Mb
31 30 ralrimivva φa𝒫Ob𝒫OMabMa+𝑒Mb
32 31 adantr φe𝒫Oa𝒫Ob𝒫OMabMa+𝑒Mb
33 uneq1 a=eABab=eABb
34 33 fveq2d a=eABMab=MeABb
35 fveq2 a=eABMa=MeAB
36 35 oveq1d a=eABMa+𝑒Mb=MeAB+𝑒Mb
37 34 36 breq12d a=eABMabMa+𝑒MbMeABbMeAB+𝑒Mb
38 uneq2 b=eAeABb=eABeA
39 38 fveq2d b=eAMeABb=MeABeA
40 fveq2 b=eAMb=MeA
41 40 oveq2d b=eAMeAB+𝑒Mb=MeAB+𝑒MeA
42 39 41 breq12d b=eAMeABbMeAB+𝑒MbMeABeAMeAB+𝑒MeA
43 37 42 rspc2v eAB𝒫OeA𝒫Oa𝒫Ob𝒫OMabMa+𝑒MbMeABeAMeAB+𝑒MeA
44 43 imp eAB𝒫OeA𝒫Oa𝒫Ob𝒫OMabMa+𝑒MbMeABeAMeAB+𝑒MeA
45 18 21 32 44 syl21anc φe𝒫OMeABeAMeAB+𝑒MeA
46 29 45 eqbrtrrid φe𝒫OMeABMeAB+𝑒MeA
47 xleadd2a MeAB*MeAB+𝑒MeA*MeAB*MeABMeAB+𝑒MeAMeAB+𝑒MeABMeAB+𝑒MeAB+𝑒MeA
48 16 24 27 46 47 syl31anc φe𝒫OMeAB+𝑒MeABMeAB+𝑒MeAB+𝑒MeA
49 1 2 elcarsg φBtoCaraSigaMBOf𝒫OMfB+𝑒MfB=Mf
50 5 49 mpbid φBOf𝒫OMfB+𝑒MfB=Mf
51 50 simprd φf𝒫OMfB+𝑒MfB=Mf
52 51 adantr φe𝒫Of𝒫OMfB+𝑒MfB=Mf
53 ineq1 f=eAfB=eAB
54 53 fveq2d f=eAMfB=MeAB
55 difeq1 f=eAfB=eAB
56 55 fveq2d f=eAMfB=MeAB
57 54 56 oveq12d f=eAMfB+𝑒MfB=MeAB+𝑒MeAB
58 fveq2 f=eAMf=MeA
59 57 58 eqeq12d f=eAMfB+𝑒MfB=MfMeAB+𝑒MeAB=MeA
60 59 adantl φe𝒫Of=eAMfB+𝑒MfB=MfMeAB+𝑒MeAB=MeA
61 17 60 rspcdv φe𝒫Of𝒫OMfB+𝑒MfB=MfMeAB+𝑒MeAB=MeA
62 52 61 mpd φe𝒫OMeAB+𝑒MeAB=MeA
63 62 oveq1d φe𝒫OMeAB+𝑒MeAB+𝑒MeA=MeA+𝑒MeA
64 17 elpwincl1 φe𝒫OeAB𝒫O
65 12 64 ffvelrnd φe𝒫OMeAB0+∞
66 xrge0addass MeAB0+∞MeAB0+∞MeA0+∞MeAB+𝑒MeAB+𝑒MeA=MeAB+𝑒MeAB+𝑒MeA
67 65 19 22 66 syl3anc φe𝒫OMeAB+𝑒MeAB+𝑒MeA=MeAB+𝑒MeAB+𝑒MeA
68 inass eAB=eAB
69 68 fveq2i MeAB=MeAB
70 69 oveq1i MeAB+𝑒MeAB+𝑒MeA=MeAB+𝑒MeAB+𝑒MeA
71 67 70 eqtrdi φe𝒫OMeAB+𝑒MeAB+𝑒MeA=MeAB+𝑒MeAB+𝑒MeA
72 7 simprd φe𝒫OMeA+𝑒MeA=Me
73 72 r19.21bi φe𝒫OMeA+𝑒MeA=Me
74 63 71 73 3eqtr3d φe𝒫OMeAB+𝑒MeAB+𝑒MeA=Me
75 48 74 breqtrd φe𝒫OMeAB+𝑒MeABMe
76 inundif eABeAB=e
77 76 fveq2i MeABeAB=Me
78 uneq1 a=eABab=eABb
79 78 fveq2d a=eABMab=MeABb
80 fveq2 a=eABMa=MeAB
81 80 oveq1d a=eABMa+𝑒Mb=MeAB+𝑒Mb
82 79 81 breq12d a=eABMabMa+𝑒MbMeABbMeAB+𝑒Mb
83 uneq2 b=eABeABb=eABeAB
84 83 fveq2d b=eABMeABb=MeABeAB
85 fveq2 b=eABMb=MeAB
86 85 oveq2d b=eABMeAB+𝑒Mb=MeAB+𝑒MeAB
87 84 86 breq12d b=eABMeABbMeAB+𝑒MbMeABeABMeAB+𝑒MeAB
88 82 87 rspc2v eAB𝒫OeAB𝒫Oa𝒫Ob𝒫OMabMa+𝑒MbMeABeABMeAB+𝑒MeAB
89 88 imp eAB𝒫OeAB𝒫Oa𝒫Ob𝒫OMabMa+𝑒MbMeABeABMeAB+𝑒MeAB
90 25 14 32 89 syl21anc φe𝒫OMeABeABMeAB+𝑒MeAB
91 77 90 eqbrtrrid φe𝒫OMeMeAB+𝑒MeAB
92 75 91 jca φe𝒫OMeAB+𝑒MeABMeMeMeAB+𝑒MeAB
93 27 16 xaddcld φe𝒫OMeAB+𝑒MeAB*
94 2 ffvelrnda φe𝒫OMe0+∞
95 11 94 sselid φe𝒫OMe*
96 xrletri3 MeAB+𝑒MeAB*Me*MeAB+𝑒MeAB=MeMeAB+𝑒MeABMeMeMeAB+𝑒MeAB
97 93 95 96 syl2anc φe𝒫OMeAB+𝑒MeAB=MeMeAB+𝑒MeABMeMeMeAB+𝑒MeAB
98 92 97 mpbird φe𝒫OMeAB+𝑒MeAB=Me
99 98 ralrimiva φe𝒫OMeAB+𝑒MeAB=Me
100 10 99 jca φABOe𝒫OMeAB+𝑒MeAB=Me
101 1 2 elcarsg φABtoCaraSigaMABOe𝒫OMeAB+𝑒MeAB=Me
102 100 101 mpbird φABtoCaraSigaM