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 ${⊢}{\phi }\to {O}\in {V}$
carsgval.2 ${⊢}{\phi }\to {M}:𝒫{O}⟶\left[0,\mathrm{+\infty }\right]$
difelcarsg.1 ${⊢}{\phi }\to {A}\in \mathrm{toCaraSiga}\left({M}\right)$
inelcarsg.1 ${⊢}\left({\phi }\wedge {a}\in 𝒫{O}\wedge {b}\in 𝒫{O}\right)\to {M}\left({a}\cup {b}\right)\le {M}\left({a}\right){+}_{𝑒}{M}\left({b}\right)$
inelcarsg.2 ${⊢}{\phi }\to {B}\in \mathrm{toCaraSiga}\left({M}\right)$
Assertion inelcarsg ${⊢}{\phi }\to {A}\cap {B}\in \mathrm{toCaraSiga}\left({M}\right)$

Proof

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