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 sseldi ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴𝐵 ) ) ) ∈ ℝ* )
17 13 elpwincl1 ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒𝐴 ) ∈ 𝒫 𝑂 )
18 17 elpwdifcl ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒𝐴 ) ∖ 𝐵 ) ∈ 𝒫 𝑂 )
19 12 18 ffvelrnd ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( 𝑒𝐴 ) ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
20 11 19 sseldi ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( 𝑒𝐴 ) ∖ 𝐵 ) ) ∈ ℝ* )
21 13 elpwdifcl ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒𝐴 ) ∈ 𝒫 𝑂 )
22 12 21 ffvelrnd ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒𝐴 ) ) ∈ ( 0 [,] +∞ ) )
23 11 22 sseldi ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒𝐴 ) ) ∈ ℝ* )
24 20 23 xaddcld ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( ( 𝑒𝐴 ) ∖ 𝐵 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒𝐴 ) ) ) ∈ ℝ* )
25 13 elpwincl1 ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ ( 𝐴𝐵 ) ) ∈ 𝒫 𝑂 )
26 12 25 ffvelrnd ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴𝐵 ) ) ) ∈ ( 0 [,] +∞ ) )
27 11 26 sseldi ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴𝐵 ) ) ) ∈ ℝ* )
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 sseldi ( ( 𝜑𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀𝑒 ) ∈ ℝ* )
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 ‘ 𝑀 ) )