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 ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caragenuncllem.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
caragenuncllem.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
caragenuncllem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
caragenuncllem.x ⊢ 𝑋 = ∪ dom 𝑂
caragenuncllem.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
Assertion caragenuncllem ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐸 ∪ 𝐹 ) ) ) ) = ( 𝑂 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 caragenuncllem.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 caragenuncllem.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 caragenuncllem.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
4 caragenuncllem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
5 caragenuncllem.x ⊢ 𝑋 = ∪ dom 𝑂
6 caragenuncllem.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
7 6 ssinss1d ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ⊆ 𝑋 )
8 1 2 5 3 7 caragensplit ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ) )
9 8 eqcomd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 ) ) ) )
10 inass ⊢ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) = ( 𝐴 ∩ ( ( 𝐸 ∪ 𝐹 ) ∩ 𝐸 ) )
11 incom ⊢ ( ( 𝐸 ∪ 𝐹 ) ∩ 𝐸 ) = ( 𝐸 ∩ ( 𝐸 ∪ 𝐹 ) )
12 inabs ⊢ ( 𝐸 ∩ ( 𝐸 ∪ 𝐹 ) ) = 𝐸
13 11 12 eqtri ⊢ ( ( 𝐸 ∪ 𝐹 ) ∩ 𝐸 ) = 𝐸
14 13 ineq2i ⊢ ( 𝐴 ∩ ( ( 𝐸 ∪ 𝐹 ) ∩ 𝐸 ) ) = ( 𝐴 ∩ 𝐸 )
15 10 14 eqtri ⊢ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) = ( 𝐴 ∩ 𝐸 )
16 15 fveq2i ⊢ ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) ) = ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) )
17 incom ⊢ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) = ( 𝐹 ∩ ( 𝐴 ∖ 𝐸 ) )
18 indifcom ⊢ ( 𝐹 ∩ ( 𝐴 ∖ 𝐸 ) ) = ( 𝐴 ∩ ( 𝐹 ∖ 𝐸 ) )
19 17 18 eqtr2i ⊢ ( 𝐴 ∩ ( 𝐹 ∖ 𝐸 ) ) = ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 )
20 19 eqcomi ⊢ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) = ( 𝐴 ∩ ( 𝐹 ∖ 𝐸 ) )
21 difundir ⊢ ( ( 𝐸 ∪ 𝐹 ) ∖ 𝐸 ) = ( ( 𝐸 ∖ 𝐸 ) ∪ ( 𝐹 ∖ 𝐸 ) )
22 difid ⊢ ( 𝐸 ∖ 𝐸 ) = ∅
23 22 uneq1i ⊢ ( ( 𝐸 ∖ 𝐸 ) ∪ ( 𝐹 ∖ 𝐸 ) ) = ( ∅ ∪ ( 𝐹 ∖ 𝐸 ) )
24 0un ⊢ ( ∅ ∪ ( 𝐹 ∖ 𝐸 ) ) = ( 𝐹 ∖ 𝐸 )
25 21 23 24 3eqtrri ⊢ ( 𝐹 ∖ 𝐸 ) = ( ( 𝐸 ∪ 𝐹 ) ∖ 𝐸 )
26 25 ineq2i ⊢ ( 𝐴 ∩ ( 𝐹 ∖ 𝐸 ) ) = ( 𝐴 ∩ ( ( 𝐸 ∪ 𝐹 ) ∖ 𝐸 ) )
27 indif2 ⊢ ( 𝐴 ∩ ( ( 𝐸 ∪ 𝐹 ) ∖ 𝐸 ) ) = ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 )
28 20 26 27 3eqtrri ⊢ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 ) = ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 )
29 28 fveq2i ⊢ ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 ) ) = ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) )
30 16 29 oveq12i ⊢ ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) )
31 30 a1i ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ∖ 𝐸 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) )
32 eqidd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) )
33 9 31 32 3eqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) )
34 difun1 ⊢ ( 𝐴 ∖ ( 𝐸 ∪ 𝐹 ) ) = ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 )
35 34 fveq2i ⊢ ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐸 ∪ 𝐹 ) ) ) = ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) )
36 35 a1i ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐸 ∪ 𝐹 ) ) ) = ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) )
37 33 36 oveq12d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐸 ∪ 𝐹 ) ) ) ) = ( ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) )
38 6 ssinss1d ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐸 ) ⊆ 𝑋 )
39 1 5 38 omexrcl ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ∈ ℝ* )
40 1 5 38 omecl ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ∈ ( 0 [,] +∞ ) )
41 40 xrge0nemnfd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ≠ -∞ )
42 39 41 jca ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ≠ -∞ ) )
43 1 2 4 5 caragenelss ⊢ ( 𝜑 → 𝐹 ⊆ 𝑋 )
44 43 ssinss2d ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ⊆ 𝑋 )
45 1 5 44 omexrcl ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ∈ ℝ* )
46 1 5 44 omecl ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ∈ ( 0 [,] +∞ ) )
47 46 xrge0nemnfd ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ≠ -∞ )
48 45 47 jca ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ≠ -∞ ) )
49 6 ssdifssd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐸 ) ⊆ 𝑋 )
50 49 ssdifssd ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ⊆ 𝑋 )
51 1 5 50 omexrcl ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ∈ ℝ* )
52 1 5 50 omecl ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ∈ ( 0 [,] +∞ ) )
53 52 xrge0nemnfd ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ≠ -∞ )
54 51 53 jca ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ≠ -∞ ) )
55 xaddass ⊢ ( ( ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) ≠ -∞ ) ∧ ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ≠ -∞ ) ∧ ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ≠ -∞ ) ) → ( ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) ) )
56 42 48 54 55 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) ) )
57 1 2 5 4 49 caragensplit ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) )
58 57 oveq2d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) )
59 1 2 5 3 6 caragensplit ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
60 58 59 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∩ 𝐹 ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∖ 𝐸 ) ∖ 𝐹 ) ) ) ) = ( 𝑂 ‘ 𝐴 ) )
61 37 56 60 3eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ∪ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐸 ∪ 𝐹 ) ) ) ) = ( 𝑂 ‘ 𝐴 ) )