# Metamath Proof Explorer

## Theorem caragenuncllem

Description: The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragenuncllem.o ${⊢}{\phi }\to {O}\in \mathrm{OutMeas}$
caragenuncllem.s ${⊢}{S}=\mathrm{CaraGen}\left({O}\right)$
caragenuncllem.e ${⊢}{\phi }\to {E}\in {S}$
caragenuncllem.f ${⊢}{\phi }\to {F}\in {S}$
caragenuncllem.x ${⊢}{X}=\bigcup \mathrm{dom}{O}$
caragenuncllem.a ${⊢}{\phi }\to {A}\subseteq {X}$
Assertion caragenuncllem ${⊢}{\phi }\to {O}\left({A}\cap \left({E}\cup {F}\right)\right){+}_{𝑒}{O}\left({A}\setminus \left({E}\cup {F}\right)\right)={O}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 caragenuncllem.o ${⊢}{\phi }\to {O}\in \mathrm{OutMeas}$
2 caragenuncllem.s ${⊢}{S}=\mathrm{CaraGen}\left({O}\right)$
3 caragenuncllem.e ${⊢}{\phi }\to {E}\in {S}$
4 caragenuncllem.f ${⊢}{\phi }\to {F}\in {S}$
5 caragenuncllem.x ${⊢}{X}=\bigcup \mathrm{dom}{O}$
6 caragenuncllem.a ${⊢}{\phi }\to {A}\subseteq {X}$
7 6 ssinss1d ${⊢}{\phi }\to {A}\cap \left({E}\cup {F}\right)\subseteq {X}$
8 1 2 5 3 7 caragensplit ${⊢}{\phi }\to {O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}\right)={O}\left({A}\cap \left({E}\cup {F}\right)\right)$
9 8 eqcomd ${⊢}{\phi }\to {O}\left({A}\cap \left({E}\cup {F}\right)\right)={O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}\right)$
10 inass ${⊢}\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}={A}\cap \left(\left({E}\cup {F}\right)\cap {E}\right)$
11 incom ${⊢}\left({E}\cup {F}\right)\cap {E}={E}\cap \left({E}\cup {F}\right)$
12 inabs ${⊢}{E}\cap \left({E}\cup {F}\right)={E}$
13 11 12 eqtri ${⊢}\left({E}\cup {F}\right)\cap {E}={E}$
14 13 ineq2i ${⊢}{A}\cap \left(\left({E}\cup {F}\right)\cap {E}\right)={A}\cap {E}$
15 10 14 eqtri ${⊢}\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}={A}\cap {E}$
16 15 fveq2i ${⊢}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}\right)={O}\left({A}\cap {E}\right)$
17 incom ${⊢}\left({A}\setminus {E}\right)\cap {F}={F}\cap \left({A}\setminus {E}\right)$
18 indifcom ${⊢}{F}\cap \left({A}\setminus {E}\right)={A}\cap \left({F}\setminus {E}\right)$
19 17 18 eqtr2i ${⊢}{A}\cap \left({F}\setminus {E}\right)=\left({A}\setminus {E}\right)\cap {F}$
20 19 eqcomi ${⊢}\left({A}\setminus {E}\right)\cap {F}={A}\cap \left({F}\setminus {E}\right)$
21 difundir ${⊢}\left({E}\cup {F}\right)\setminus {E}=\left({E}\setminus {E}\right)\cup \left({F}\setminus {E}\right)$
22 difid ${⊢}{E}\setminus {E}=\varnothing$
23 22 uneq1i ${⊢}\left({E}\setminus {E}\right)\cup \left({F}\setminus {E}\right)=\varnothing \cup \left({F}\setminus {E}\right)$
24 0un ${⊢}\varnothing \cup \left({F}\setminus {E}\right)={F}\setminus {E}$
25 21 23 24 3eqtrri ${⊢}{F}\setminus {E}=\left({E}\cup {F}\right)\setminus {E}$
26 25 ineq2i ${⊢}{A}\cap \left({F}\setminus {E}\right)={A}\cap \left(\left({E}\cup {F}\right)\setminus {E}\right)$
27 indif2 ${⊢}{A}\cap \left(\left({E}\cup {F}\right)\setminus {E}\right)=\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}$
28 20 26 27 3eqtrri ${⊢}\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}=\left({A}\setminus {E}\right)\cap {F}$
29 28 fveq2i ${⊢}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}\right)={O}\left(\left({A}\setminus {E}\right)\cap {F}\right)$
30 16 29 oveq12i ${⊢}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}\right)={O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)$
31 30 a1i ${⊢}{\phi }\to {O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\cap \left({E}\cup {F}\right)\right)\setminus {E}\right)={O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)$
32 eqidd ${⊢}{\phi }\to {O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)={O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)$
33 9 31 32 3eqtrd ${⊢}{\phi }\to {O}\left({A}\cap \left({E}\cup {F}\right)\right)={O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)$
34 difun1 ${⊢}{A}\setminus \left({E}\cup {F}\right)=\left({A}\setminus {E}\right)\setminus {F}$
35 34 fveq2i ${⊢}{O}\left({A}\setminus \left({E}\cup {F}\right)\right)={O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)$
36 35 a1i ${⊢}{\phi }\to {O}\left({A}\setminus \left({E}\cup {F}\right)\right)={O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)$
37 33 36 oveq12d ${⊢}{\phi }\to {O}\left({A}\cap \left({E}\cup {F}\right)\right){+}_{𝑒}{O}\left({A}\setminus \left({E}\cup {F}\right)\right)=\left({O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)$
38 6 ssinss1d ${⊢}{\phi }\to {A}\cap {E}\subseteq {X}$
39 1 5 38 omexrcl ${⊢}{\phi }\to {O}\left({A}\cap {E}\right)\in {ℝ}^{*}$
40 1 5 38 omecl ${⊢}{\phi }\to {O}\left({A}\cap {E}\right)\in \left[0,\mathrm{+\infty }\right]$
41 40 xrge0nemnfd ${⊢}{\phi }\to {O}\left({A}\cap {E}\right)\ne \mathrm{-\infty }$
42 39 41 jca ${⊢}{\phi }\to \left({O}\left({A}\cap {E}\right)\in {ℝ}^{*}\wedge {O}\left({A}\cap {E}\right)\ne \mathrm{-\infty }\right)$
43 1 2 4 5 caragenelss ${⊢}{\phi }\to {F}\subseteq {X}$
44 43 ssinss2d ${⊢}{\phi }\to \left({A}\setminus {E}\right)\cap {F}\subseteq {X}$
45 1 5 44 omexrcl ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\in {ℝ}^{*}$
46 1 5 44 omecl ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\in \left[0,\mathrm{+\infty }\right]$
47 46 xrge0nemnfd ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\ne \mathrm{-\infty }$
48 45 47 jca ${⊢}{\phi }\to \left({O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\in {ℝ}^{*}\wedge {O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\ne \mathrm{-\infty }\right)$
49 6 ssdifssd ${⊢}{\phi }\to {A}\setminus {E}\subseteq {X}$
50 49 ssdifssd ${⊢}{\phi }\to \left({A}\setminus {E}\right)\setminus {F}\subseteq {X}$
51 1 5 50 omexrcl ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\in {ℝ}^{*}$
52 1 5 50 omecl ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\in \left[0,\mathrm{+\infty }\right]$
53 52 xrge0nemnfd ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\ne \mathrm{-\infty }$
54 51 53 jca ${⊢}{\phi }\to \left({O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\in {ℝ}^{*}\wedge {O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\ne \mathrm{-\infty }\right)$
55 xaddass ${⊢}\left(\left({O}\left({A}\cap {E}\right)\in {ℝ}^{*}\wedge {O}\left({A}\cap {E}\right)\ne \mathrm{-\infty }\right)\wedge \left({O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\in {ℝ}^{*}\wedge {O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\ne \mathrm{-\infty }\right)\wedge \left({O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\in {ℝ}^{*}\wedge {O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\ne \mathrm{-\infty }\right)\right)\to \left({O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)={O}\left({A}\cap {E}\right){+}_{𝑒}\left({O}\left(\left({A}\setminus {E}\right)\cap {F}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\right)$
56 42 48 54 55 syl3anc ${⊢}{\phi }\to \left({O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\cap {F}\right)\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)={O}\left({A}\cap {E}\right){+}_{𝑒}\left({O}\left(\left({A}\setminus {E}\right)\cap {F}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\right)$
57 1 2 5 4 49 caragensplit ${⊢}{\phi }\to {O}\left(\left({A}\setminus {E}\right)\cap {F}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)={O}\left({A}\setminus {E}\right)$
58 57 oveq2d ${⊢}{\phi }\to {O}\left({A}\cap {E}\right){+}_{𝑒}\left({O}\left(\left({A}\setminus {E}\right)\cap {F}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\right)={O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left({A}\setminus {E}\right)$
59 1 2 5 3 6 caragensplit ${⊢}{\phi }\to {O}\left({A}\cap {E}\right){+}_{𝑒}{O}\left({A}\setminus {E}\right)={O}\left({A}\right)$
60 58 59 eqtrd ${⊢}{\phi }\to {O}\left({A}\cap {E}\right){+}_{𝑒}\left({O}\left(\left({A}\setminus {E}\right)\cap {F}\right){+}_{𝑒}{O}\left(\left({A}\setminus {E}\right)\setminus {F}\right)\right)={O}\left({A}\right)$
61 37 56 60 3eqtrd ${⊢}{\phi }\to {O}\left({A}\cap \left({E}\cup {F}\right)\right){+}_{𝑒}{O}\left({A}\setminus \left({E}\cup {F}\right)\right)={O}\left({A}\right)$