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 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
difelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
inelcarsg.1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +𝑒 ( 𝑀 ‘ 𝑏 ) ) )
inelcarsg.2 ⊢ ( 𝜑 → 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) )
Assertion inelcarsg ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

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