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 φ O V
carsgval.2 φ M : 𝒫 O 0 +∞
difelcarsg.1 φ A toCaraSiga M
inelcarsg.1 φ a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b
inelcarsg.2 φ B toCaraSiga M
Assertion inelcarsg φ A B toCaraSiga M

Proof

Step Hyp Ref Expression
1 carsgval.1 φ O V
2 carsgval.2 φ M : 𝒫 O 0 +∞
3 difelcarsg.1 φ A toCaraSiga M
4 inelcarsg.1 φ a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b
5 inelcarsg.2 φ B toCaraSiga M
6 1 2 elcarsg φ A toCaraSiga M A O e 𝒫 O M e A + 𝑒 M e A = M e
7 3 6 mpbid φ A O e 𝒫 O M e A + 𝑒 M e A = M e
8 7 simpld φ A O
9 ssinss1 A O A B O
10 8 9 syl φ A B O
11 iccssxr 0 +∞ *
12 2 adantr φ e 𝒫 O M : 𝒫 O 0 +∞
13 simpr φ e 𝒫 O e 𝒫 O
14 13 elpwdifcl φ e 𝒫 O e A B 𝒫 O
15 12 14 ffvelrnd φ e 𝒫 O M e A B 0 +∞
16 11 15 sseldi φ e 𝒫 O M e A B *
17 13 elpwincl1 φ e 𝒫 O e A 𝒫 O
18 17 elpwdifcl φ e 𝒫 O e A B 𝒫 O
19 12 18 ffvelrnd φ e 𝒫 O M e A B 0 +∞
20 11 19 sseldi φ e 𝒫 O M e A B *
21 13 elpwdifcl φ e 𝒫 O e A 𝒫 O
22 12 21 ffvelrnd φ e 𝒫 O M e A 0 +∞
23 11 22 sseldi φ e 𝒫 O M e A *
24 20 23 xaddcld φ e 𝒫 O M e A B + 𝑒 M e A *
25 13 elpwincl1 φ e 𝒫 O e A B 𝒫 O
26 12 25 ffvelrnd φ e 𝒫 O M e A B 0 +∞
27 11 26 sseldi φ e 𝒫 O M e A B *
28 indifundif e A B e A = e A B
29 28 fveq2i M e A B e A = M e A B
30 4 3expb φ a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b
31 30 ralrimivva φ a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b
32 31 adantr φ e 𝒫 O a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b
33 uneq1 a = e A B a b = e A B b
34 33 fveq2d a = e A B M a b = M e A B b
35 fveq2 a = e A B M a = M e A B
36 35 oveq1d a = e A B M a + 𝑒 M b = M e A B + 𝑒 M b
37 34 36 breq12d a = e A B M a b M a + 𝑒 M b M e A B b M e A B + 𝑒 M b
38 uneq2 b = e A e A B b = e A B e A
39 38 fveq2d b = e A M e A B b = M e A B e A
40 fveq2 b = e A M b = M e A
41 40 oveq2d b = e A M e A B + 𝑒 M b = M e A B + 𝑒 M e A
42 39 41 breq12d b = e A M e A B b M e A B + 𝑒 M b M e A B e A M e A B + 𝑒 M e A
43 37 42 rspc2v e A B 𝒫 O e A 𝒫 O a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b M e A B e A M e A B + 𝑒 M e A
44 43 imp e A B 𝒫 O e A 𝒫 O a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b M e A B e A M e A B + 𝑒 M e A
45 18 21 32 44 syl21anc φ e 𝒫 O M e A B e A M e A B + 𝑒 M e A
46 29 45 eqbrtrrid φ e 𝒫 O M e A B M e A B + 𝑒 M e A
47 xleadd2a M e A B * M e A B + 𝑒 M e A * M e A B * M e A B M e A B + 𝑒 M e A M e A B + 𝑒 M e A B M e A B + 𝑒 M e A B + 𝑒 M e A
48 16 24 27 46 47 syl31anc φ e 𝒫 O M e A B + 𝑒 M e A B M e A B + 𝑒 M e A B + 𝑒 M e A
49 1 2 elcarsg φ B toCaraSiga M B O f 𝒫 O M f B + 𝑒 M f B = M f
50 5 49 mpbid φ B O f 𝒫 O M f B + 𝑒 M f B = M f
51 50 simprd φ f 𝒫 O M f B + 𝑒 M f B = M f
52 51 adantr φ e 𝒫 O f 𝒫 O M f B + 𝑒 M f B = M f
53 ineq1 f = e A f B = e A B
54 53 fveq2d f = e A M f B = M e A B
55 difeq1 f = e A f B = e A B
56 55 fveq2d f = e A M f B = M e A B
57 54 56 oveq12d f = e A M f B + 𝑒 M f B = M e A B + 𝑒 M e A B
58 fveq2 f = e A M f = M e A
59 57 58 eqeq12d f = e A M f B + 𝑒 M f B = M f M e A B + 𝑒 M e A B = M e A
60 59 adantl φ e 𝒫 O f = e A M f B + 𝑒 M f B = M f M e A B + 𝑒 M e A B = M e A
61 17 60 rspcdv φ e 𝒫 O f 𝒫 O M f B + 𝑒 M f B = M f M e A B + 𝑒 M e A B = M e A
62 52 61 mpd φ e 𝒫 O M e A B + 𝑒 M e A B = M e A
63 62 oveq1d φ e 𝒫 O M e A B + 𝑒 M e A B + 𝑒 M e A = M e A + 𝑒 M e A
64 17 elpwincl1 φ e 𝒫 O e A B 𝒫 O
65 12 64 ffvelrnd φ e 𝒫 O M e A B 0 +∞
66 xrge0addass M e A B 0 +∞ M e A B 0 +∞ M e A 0 +∞ M e A B + 𝑒 M e A B + 𝑒 M e A = M e A B + 𝑒 M e A B + 𝑒 M e A
67 65 19 22 66 syl3anc φ e 𝒫 O M e A B + 𝑒 M e A B + 𝑒 M e A = M e A B + 𝑒 M e A B + 𝑒 M e A
68 inass e A B = e A B
69 68 fveq2i M e A B = M e A B
70 69 oveq1i M e A B + 𝑒 M e A B + 𝑒 M e A = M e A B + 𝑒 M e A B + 𝑒 M e A
71 67 70 syl6eq φ e 𝒫 O M e A B + 𝑒 M e A B + 𝑒 M e A = M e A B + 𝑒 M e A B + 𝑒 M e A
72 7 simprd φ e 𝒫 O M e A + 𝑒 M e A = M e
73 72 r19.21bi φ e 𝒫 O M e A + 𝑒 M e A = M e
74 63 71 73 3eqtr3d φ e 𝒫 O M e A B + 𝑒 M e A B + 𝑒 M e A = M e
75 48 74 breqtrd φ e 𝒫 O M e A B + 𝑒 M e A B M e
76 inundif e A B e A B = e
77 76 fveq2i M e A B e A B = M e
78 uneq1 a = e A B a b = e A B b
79 78 fveq2d a = e A B M a b = M e A B b
80 fveq2 a = e A B M a = M e A B
81 80 oveq1d a = e A B M a + 𝑒 M b = M e A B + 𝑒 M b
82 79 81 breq12d a = e A B M a b M a + 𝑒 M b M e A B b M e A B + 𝑒 M b
83 uneq2 b = e A B e A B b = e A B e A B
84 83 fveq2d b = e A B M e A B b = M e A B e A B
85 fveq2 b = e A B M b = M e A B
86 85 oveq2d b = e A B M e A B + 𝑒 M b = M e A B + 𝑒 M e A B
87 84 86 breq12d b = e A B M e A B b M e A B + 𝑒 M b M e A B e A B M e A B + 𝑒 M e A B
88 82 87 rspc2v e A B 𝒫 O e A B 𝒫 O a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b M e A B e A B M e A B + 𝑒 M e A B
89 88 imp e A B 𝒫 O e A B 𝒫 O a 𝒫 O b 𝒫 O M a b M a + 𝑒 M b M e A B e A B M e A B + 𝑒 M e A B
90 25 14 32 89 syl21anc φ e 𝒫 O M e A B e A B M e A B + 𝑒 M e A B
91 77 90 eqbrtrrid φ e 𝒫 O M e M e A B + 𝑒 M e A B
92 75 91 jca φ e 𝒫 O M e A B + 𝑒 M e A B M e M e M e A B + 𝑒 M e A B
93 27 16 xaddcld φ e 𝒫 O M e A B + 𝑒 M e A B *
94 2 ffvelrnda φ e 𝒫 O M e 0 +∞
95 11 94 sseldi φ e 𝒫 O M e *
96 xrletri3 M e A B + 𝑒 M e A B * M e * M e A B + 𝑒 M e A B = M e M e A B + 𝑒 M e A B M e M e M e A B + 𝑒 M e A B
97 93 95 96 syl2anc φ e 𝒫 O M e A B + 𝑒 M e A B = M e M e A B + 𝑒 M e A B M e M e M e A B + 𝑒 M e A B
98 92 97 mpbird φ e 𝒫 O M e A B + 𝑒 M e A B = M e
99 98 ralrimiva φ e 𝒫 O M e A B + 𝑒 M e A B = M e
100 10 99 jca φ A B O e 𝒫 O M e A B + 𝑒 M e A B = M e
101 1 2 elcarsg φ A B toCaraSiga M A B O e 𝒫 O M e A B + 𝑒 M e A B = M e
102 100 101 mpbird φ A B toCaraSiga M