Metamath Proof Explorer

Theorem carsgclctun

Description: The Caratheodory measurable sets are closed under countable union. (Contributed by Thierry Arnoux, 21-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
carsgclctun.1 ⊢ ( 𝜑 → 𝐴 ≼ ω )
carsgclctun.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
Assertion carsgclctun ( 𝜑 → ∪ 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
6 carsgclctun.1 ⊢ ( 𝜑 → 𝐴 ≼ ω )
7 carsgclctun.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
8 7 unissd ⊢ ( 𝜑 → ∪ 𝐴 ⊆ ∪ ( toCaraSiga ‘ 𝑀 ) )
9 1 2 3 carsguni ⊢ ( 𝜑 → ∪ ( toCaraSiga ‘ 𝑀 ) = 𝑂 )
10 8 9 sseqtrd ⊢ ( 𝜑 → ∪ 𝐴 ⊆ 𝑂 )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑂 ∈ 𝑉 )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∅ ) = 0 )
14 4 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
15 5 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝐴 ≼ ω )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑒 ∈ 𝒫 𝑂 )
19 11 12 13 14 15 16 17 18 carsgclctunlem3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) )
20 inex1g ⊢ ( 𝑒 ∈ 𝒫 𝑂 → ( 𝑒 ∩ ∪ 𝐴 ) ∈ V )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ ∪ 𝐴 ) ∈ V )
22 difexg ⊢ ( 𝑒 ∈ 𝒫 𝑂 → ( 𝑒 ∖ ∪ 𝐴 ) ∈ V )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ ∪ 𝐴 ) ∈ V )
24 prct ⊢ ( ( ( 𝑒 ∩ ∪ 𝐴 ) ∈ V ∧ ( 𝑒 ∖ ∪ 𝐴 ) ∈ V ) → { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω )
25 21 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω )
26 18 elpwincl1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ ∪ 𝐴 ) ∈ 𝒫 𝑂 )
27 18 elpwdifcl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ ∪ 𝐴 ) ∈ 𝒫 𝑂 )
28 prssi ⊢ ( ( ( 𝑒 ∩ ∪ 𝐴 ) ∈ 𝒫 𝑂 ∧ ( 𝑒 ∖ ∪ 𝐴 ) ∈ 𝒫 𝑂 ) → { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 )
29 26 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 )
30 prex ⊢ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ∈ V
31 breq1 ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ( 𝑥 ≼ ω ↔ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω ) )
32 sseq1 ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ( 𝑥 ⊆ 𝒫 𝑂 ↔ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 ) )
33 31 32 3anbi23d ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) ↔ ( 𝜑 ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 ) ) )
34 unieq ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ∪ 𝑥 = ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } )
35 34 fveq2d ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) )
36 esumeq1 ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) = Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) )
37 35 36 breq12d ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ( ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) ≤ Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) ) )
38 33 37 imbi12d ⊢ ( 𝑥 = { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } → ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) ≤ Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) ) ) )
39 38 4 vtoclg ⊢ ( { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ∈ V → ( ( 𝜑 ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) ≤ Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) ) )
40 30 39 ax-mp ⊢ ( ( 𝜑 ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) ≤ Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) )
41 40 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ≼ ω ∧ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) ≤ Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) )
42 25 29 41 mpd3an23 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) ≤ Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) )
43 uniprg ⊢ ( ( ( 𝑒 ∩ ∪ 𝐴 ) ∈ 𝒫 𝑂 ∧ ( 𝑒 ∖ ∪ 𝐴 ) ∈ 𝒫 𝑂 ) → ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } = ( ( 𝑒 ∩ ∪ 𝐴 ) ∪ ( 𝑒 ∖ ∪ 𝐴 ) ) )
44 26 27 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } = ( ( 𝑒 ∩ ∪ 𝐴 ) ∪ ( 𝑒 ∖ ∪ 𝐴 ) ) )
45 inundif ⊢ ( ( 𝑒 ∩ ∪ 𝐴 ) ∪ ( 𝑒 ∖ ∪ 𝐴 ) ) = 𝑒
46 44 45 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } = 𝑒 )
47 46 fveq2d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ) = ( 𝑀 ‘ 𝑒 ) )
48 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑦 = ( 𝑒 ∩ ∪ 𝐴 ) ) → 𝑦 = ( 𝑒 ∩ ∪ 𝐴 ) )
49 48 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑦 = ( 𝑒 ∩ ∪ 𝐴 ) ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) )
50 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑦 = ( 𝑒 ∖ ∪ 𝐴 ) ) → 𝑦 = ( 𝑒 ∖ ∪ 𝐴 ) )
51 50 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑦 = ( 𝑒 ∖ ∪ 𝐴 ) ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) )
52 12 26 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
53 12 27 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
54 ineq2 ⊢ ( ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) → ( ( 𝑒 ∩ ∪ 𝐴 ) ∩ ( 𝑒 ∩ ∪ 𝐴 ) ) = ( ( 𝑒 ∩ ∪ 𝐴 ) ∩ ( 𝑒 ∖ ∪ 𝐴 ) ) )
55 inidm ⊢ ( ( 𝑒 ∩ ∪ 𝐴 ) ∩ ( 𝑒 ∩ ∪ 𝐴 ) ) = ( 𝑒 ∩ ∪ 𝐴 )
56 inindif ⊢ ( ( 𝑒 ∩ ∪ 𝐴 ) ∩ ( 𝑒 ∖ ∪ 𝐴 ) ) = ∅
57 54 55 56 3eqtr3g ⊢ ( ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) → ( 𝑒 ∩ ∪ 𝐴 ) = ∅ )
58 57 adantl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) ) → ( 𝑒 ∩ ∪ 𝐴 ) = ∅ )
59 58 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) = ( 𝑀 ‘ ∅ ) )
60 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) ) → ( 𝑀 ‘ ∅ ) = 0 )
61 59 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) = 0 )
62 61 orcd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) = 0 ∨ ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) = +∞ ) )
63 62 ex ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒 ∩ ∪ 𝐴 ) = ( 𝑒 ∖ ∪ 𝐴 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) = 0 ∨ ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) = +∞ ) ) )
64 49 51 26 27 52 53 63 esumpr2 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → Σ* 𝑦 ∈ { ( 𝑒 ∩ ∪ 𝐴 ) , ( 𝑒 ∖ ∪ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) = ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) )
65 42 47 64 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) )
66 19 65 jca ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) ∧ ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ) )
67 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
68 67 52 sselid ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) ∈ ℝ* )
69 67 53 sselid ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ∈ ℝ* )
70 68 69 xaddcld ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* )
71 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ( 0 [,] +∞ ) )
72 67 71 sselid ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ℝ* )
73 xrletri3 ⊢ ( ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝑒 ) ∈ ℝ* ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) ∧ ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ) ) )
74 70 72 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) ∧ ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) ) ) )
75 66 74 mpbird ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
76 75 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
77 1 2 elcarsg ⊢ ( 𝜑 → ( ∪ 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∪ 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
78 10 76 77 mpbir2and ⊢ ( 𝜑 → ∪ 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )