Metamath Proof Explorer

Theorem caragendifcl

Description: The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragendifcl.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caragendifcl.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
caragendifcl.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
Assertion caragendifcl ( 𝜑 → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 caragendifcl.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 caragendifcl.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 caragendifcl.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
4 eqid ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
5 2 caragenss ⊢ ( 𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂 )
6 1 5 syl ⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
7 6 unissd ⊢ ( 𝜑 → ∪ 𝑆 ⊆ ∪ dom 𝑂 )
8 7 ssdifssd ⊢ ( 𝜑 → ( ∪ 𝑆 ∖ 𝐸 ) ⊆ ∪ dom 𝑂 )
9 2 fvexi ⊢ 𝑆 ∈ V
10 9 uniex ⊢ ∪ 𝑆 ∈ V
11 difexg ⊢ ( ∪ 𝑆 ∈ V → ( ∪ 𝑆 ∖ 𝐸 ) ∈ V )
12 10 11 ax-mp ⊢ ( ∪ 𝑆 ∖ 𝐸 ) ∈ V
13 12 a1i ⊢ ( 𝜑 → ( ∪ 𝑆 ∖ 𝐸 ) ∈ V )
14 elpwg ⊢ ( ( ∪ 𝑆 ∖ 𝐸 ) ∈ V → ( ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝒫 ∪ dom 𝑂 ↔ ( ∪ 𝑆 ∖ 𝐸 ) ⊆ ∪ dom 𝑂 ) )
15 13 14 syl ⊢ ( 𝜑 → ( ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝒫 ∪ dom 𝑂 ↔ ( ∪ 𝑆 ∖ 𝐸 ) ⊆ ∪ dom 𝑂 ) )
16 8 15 mpbird ⊢ ( 𝜑 → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝒫 ∪ dom 𝑂 )
17 elpwi ⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom 𝑂 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑎 ⊆ ∪ dom 𝑂 )
19 1 2 caragenuni ⊢ ( 𝜑 → ∪ 𝑆 = ∪ dom 𝑂 )
20 19 eqcomd ⊢ ( 𝜑 → ∪ dom 𝑂 = ∪ 𝑆 )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ∪ dom 𝑂 = ∪ 𝑆 )
22 18 21 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑎 ⊆ ∪ 𝑆 )
23 difin2 ⊢ ( 𝑎 ⊆ ∪ 𝑆 → ( 𝑎 ∖ 𝐸 ) = ( ( ∪ 𝑆 ∖ 𝐸 ) ∩ 𝑎 ) )
24 22 23 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ 𝐸 ) = ( ( ∪ 𝑆 ∖ 𝐸 ) ∩ 𝑎 ) )
25 incom ⊢ ( ( ∪ 𝑆 ∖ 𝐸 ) ∩ 𝑎 ) = ( 𝑎 ∩ ( ∪ 𝑆 ∖ 𝐸 ) )
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( ∪ 𝑆 ∖ 𝐸 ) ∩ 𝑎 ) = ( 𝑎 ∩ ( ∪ 𝑆 ∖ 𝐸 ) ) )
27 24 26 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∩ ( ∪ 𝑆 ∖ 𝐸 ) ) = ( 𝑎 ∖ 𝐸 ) )
28 27 fveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∩ ( ∪ 𝑆 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) )
29 22 ssdifd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ 𝐸 ) ⊆ ( ∪ 𝑆 ∖ 𝐸 ) )
30 sscon ⊢ ( ( 𝑎 ∖ 𝐸 ) ⊆ ( ∪ 𝑆 ∖ 𝐸 ) → ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) ⊆ ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) ⊆ ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) ) )
32 dfin4 ⊢ ( 𝑎 ∩ 𝐸 ) = ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) )
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∩ 𝐸 ) = ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) ) )
34 eqimss2 ⊢ ( ( 𝑎 ∩ 𝐸 ) = ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) ) → ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) ) ⊆ ( 𝑎 ∩ 𝐸 ) )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ ( 𝑎 ∖ 𝐸 ) ) ⊆ ( 𝑎 ∩ 𝐸 ) )
36 31 35 sstrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) ⊆ ( 𝑎 ∩ 𝐸 ) )
37 elinel1 ⊢ ( 𝑥 ∈ ( 𝑎 ∩ 𝐸 ) → 𝑥 ∈ 𝑎 )
38 elinel2 ⊢ ( 𝑥 ∈ ( 𝑎 ∩ 𝐸 ) → 𝑥 ∈ 𝐸 )
39 elndif ⊢ ( 𝑥 ∈ 𝐸 → ¬ 𝑥 ∈ ( ∪ 𝑆 ∖ 𝐸 ) )
40 38 39 syl ⊢ ( 𝑥 ∈ ( 𝑎 ∩ 𝐸 ) → ¬ 𝑥 ∈ ( ∪ 𝑆 ∖ 𝐸 ) )
41 37 40 eldifd ⊢ ( 𝑥 ∈ ( 𝑎 ∩ 𝐸 ) → 𝑥 ∈ ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
42 41 ssriv ⊢ ( 𝑎 ∩ 𝐸 ) ⊆ ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) )
43 42 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∩ 𝐸 ) ⊆ ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
44 36 43 eqssd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) = ( 𝑎 ∩ 𝐸 ) )
45 44 fveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) )
46 28 45 oveq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ( ∪ 𝑆 ∖ 𝐸 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) ) ) = ( ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) ) )
47 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
48 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑂 ∈ OutMeas )
49 18 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ 𝐸 ) ⊆ ∪ dom 𝑂 )
50 48 4 49 omecl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ∈ ( 0 [,] +∞ ) )
51 47 50 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ∈ ℝ* )
52 ssinss1 ⊢ ( 𝑎 ⊆ ∪ dom 𝑂 → ( 𝑎 ∩ 𝐸 ) ⊆ ∪ dom 𝑂 )
53 17 52 syl ⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → ( 𝑎 ∩ 𝐸 ) ⊆ ∪ dom 𝑂 )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∩ 𝐸 ) ⊆ ∪ dom 𝑂 )
55 48 4 54 omecl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) ∈ ( 0 [,] +∞ ) )
56 47 55 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) ∈ ℝ* )
57 51 56 xaddcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) ) = ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) )
58 1 2 caragenel ⊢ ( 𝜑 → ( 𝐸 ∈ 𝑆 ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) ) )
59 3 58 mpbid ⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
60 59 simprd ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
61 60 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
62 46 57 61 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ( ∪ 𝑆 ∖ 𝐸 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) ) ) = ( 𝑂 ‘ 𝑎 ) )
63 1 4 2 16 62 carageneld ⊢ ( 𝜑 → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )