Metamath Proof Explorer

Theorem omsmeas

Description: The restriction of a constructed outer measure to Caratheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses omsmeas.m ⊢ 𝑀 = ( toOMeas ‘ 𝑅 )
omsmeas.s ⊢ 𝑆 = ( toCaraSiga ‘ 𝑀 )
omsmeas.o ⊢ ( 𝜑 → 𝑄 ∈ 𝑉 )
omsmeas.r ⊢ ( 𝜑 → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
omsmeas.d ⊢ ( 𝜑 → ∅ ∈ dom 𝑅 )
omsmeas.0 ⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) = 0 )
Assertion omsmeas ( 𝜑 → ( 𝑀 ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 omsmeas.m ⊢ 𝑀 = ( toOMeas ‘ 𝑅 )
2 omsmeas.s ⊢ 𝑆 = ( toCaraSiga ‘ 𝑀 )
3 omsmeas.o ⊢ ( 𝜑 → 𝑄 ∈ 𝑉 )
4 omsmeas.r ⊢ ( 𝜑 → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
5 omsmeas.d ⊢ ( 𝜑 → ∅ ∈ dom 𝑅 )
6 omsmeas.0 ⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) = 0 )
7 omsf ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )
8 3 4 7 syl2anc ⊢ ( 𝜑 → ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )
9 1 a1i ⊢ ( 𝜑 → 𝑀 = ( toOMeas ‘ 𝑅 ) )
10 4 fdmd ⊢ ( 𝜑 → dom 𝑅 = 𝑄 )
11 10 eqcomd ⊢ ( 𝜑 → 𝑄 = dom 𝑅 )
12 11 unieqd ⊢ ( 𝜑 → ∪ 𝑄 = ∪ dom 𝑅 )
13 12 pweqd ⊢ ( 𝜑 → 𝒫 ∪ 𝑄 = 𝒫 ∪ dom 𝑅 )
14 9 13 feq12d ⊢ ( 𝜑 → ( 𝑀 : 𝒫 ∪ 𝑄 ⟶ ( 0 [,] +∞ ) ↔ ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) ) )
15 8 14 mpbird ⊢ ( 𝜑 → 𝑀 : 𝒫 ∪ 𝑄 ⟶ ( 0 [,] +∞ ) )
16 3 uniexd ⊢ ( 𝜑 → ∪ 𝑄 ∈ V )
17 16 15 carsgcl ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 ∪ 𝑄 )
18 2 17 eqsstrid ⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 ∪ 𝑄 )
19 15 18 fssresd ⊢ ( 𝜑 → ( 𝑀 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
20 1 3 4 5 6 oms0 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
21 16 15 20 0elcarsg ⊢ ( 𝜑 → ∅ ∈ ( toCaraSiga ‘ 𝑀 ) )
22 21 2 eleqtrrdi ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
23 fvres ⊢ ( ∅ ∈ 𝑆 → ( ( 𝑀 ↾ 𝑆 ) ‘ ∅ ) = ( 𝑀 ‘ ∅ ) )
24 22 23 syl ⊢ ( 𝜑 → ( ( 𝑀 ↾ 𝑆 ) ‘ ∅ ) = ( 𝑀 ‘ ∅ ) )
25 24 20 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 ↾ 𝑆 ) ‘ ∅ ) = 0 )
26 nfcv ⊢ Ⅎ 𝑔 𝑓
27 nfcv ⊢ Ⅎ 𝑓 𝑔
28 id ⊢ ( 𝑓 = 𝑔 → 𝑓 = 𝑔 )
29 26 27 28 cbvdisj ⊢ ( Disj 𝑓 ∈ 𝑒 𝑓 ↔ Disj 𝑔 ∈ 𝑒 𝑔 )
30 29 anbi2i ⊢ ( ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) ↔ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) )
31 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑄 ∈ 𝑉 )
32 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑒 ∈ 𝒫 𝑆 )
34 33 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑒 ⊆ 𝑆 )
35 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑆 ⊆ 𝒫 ∪ 𝑄 )
36 34 35 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑒 ⊆ 𝒫 ∪ 𝑄 )
37 36 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → 𝑓 ∈ 𝒫 ∪ 𝑄 )
38 37 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → 𝑓 ⊆ ∪ 𝑄 )
39 simprl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑒 ≼ ω )
40 1 31 32 38 39 omssubadd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑒 𝑓 ) ≤ Σ* 𝑓 ∈ 𝑒 ( 𝑀 ‘ 𝑓 ) )
41 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ∪ 𝑄 ∈ V )
42 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑀 : 𝒫 ∪ 𝑄 ⟶ ( 0 [,] +∞ ) )
43 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( 𝑀 ‘ ∅ ) = 0 )
44 uniiun ⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
45 44 fveq2i ⊢ ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑥 𝑦 )
46 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → 𝑄 ∈ 𝑉 )
47 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
48 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝒫 ∪ 𝑄 )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
50 48 49 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝒫 ∪ 𝑄 )
51 50 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊆ ∪ 𝑄 )
52 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → 𝑥 ≼ ω )
53 1 46 47 51 52 omssubadd ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑥 𝑦 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
54 45 53 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
55 54 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
56 55 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
57 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → 𝑄 ∈ 𝑉 )
58 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
59 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → 𝑥 ⊆ 𝑦 )
60 elpwi ⊢ ( 𝑦 ∈ 𝒫 ∪ 𝑄 → 𝑦 ⊆ ∪ 𝑄 )
61 60 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → 𝑦 ⊆ ∪ 𝑄 )
62 1 57 58 59 61 omsmon ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
63 62 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
64 63 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 ∪ 𝑄 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
65 elpwi ⊢ ( 𝑒 ∈ 𝒫 𝑆 → 𝑒 ⊆ 𝑆 )
66 65 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑒 ⊆ 𝑆 )
67 66 2 sseqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → 𝑒 ⊆ ( toCaraSiga ‘ 𝑀 ) )
68 41 42 43 56 64 39 67 carsgclctun ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ∪ 𝑒 ∈ ( toCaraSiga ‘ 𝑀 ) )
69 68 2 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ∪ 𝑒 ∈ 𝑆 )
70 fvres ⊢ ( ∪ 𝑒 ∈ 𝑆 → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = ( 𝑀 ‘ ∪ 𝑒 ) )
71 uniiun ⊢ ∪ 𝑒 = ∪ 𝑓 ∈ 𝑒 𝑓
72 71 fveq2i ⊢ ( 𝑀 ‘ ∪ 𝑒 ) = ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑒 𝑓 )
73 70 72 eqtrdi ⊢ ( ∪ 𝑒 ∈ 𝑆 → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑒 𝑓 ) )
74 69 73 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑒 𝑓 ) )
75 nfv ⊢ Ⅎ 𝑓 ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) )
76 66 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → 𝑓 ∈ 𝑆 )
77 fvres ⊢ ( 𝑓 ∈ 𝑆 → ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) = ( 𝑀 ‘ 𝑓 ) )
78 76 77 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) = ( 𝑀 ‘ 𝑓 ) )
79 78 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ∀ 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) = ( 𝑀 ‘ 𝑓 ) )
80 75 79 esumeq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) = Σ* 𝑓 ∈ 𝑒 ( 𝑀 ‘ 𝑓 ) )
81 40 74 80 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ≤ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) )
82 snex ⊢ { ∅ } ∈ V
83 82 a1i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → { ∅ } ∈ V )
84 42 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → 𝑀 : 𝒫 ∪ 𝑄 ⟶ ( 0 [,] +∞ ) )
85 84 37 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → ( 𝑀 ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
86 elsni ⊢ ( 𝑓 ∈ { ∅ } → 𝑓 = ∅ )
87 86 fveq2d ⊢ ( 𝑓 ∈ { ∅ } → ( 𝑀 ‘ 𝑓 ) = ( 𝑀 ‘ ∅ ) )
88 87 43 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑓 ) = 0 )
89 33 83 85 88 esumpad2 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ ( 𝑒 ∖ { ∅ } ) ( 𝑀 ‘ 𝑓 ) = Σ* 𝑓 ∈ 𝑒 ( 𝑀 ‘ 𝑓 ) )
90 neldifsnd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ¬ ∅ ∈ ( 𝑒 ∖ { ∅ } ) )
91 difss ⊢ ( 𝑒 ∖ { ∅ } ) ⊆ 𝑒
92 ssdomg ⊢ ( 𝑒 ∈ 𝒫 𝑆 → ( ( 𝑒 ∖ { ∅ } ) ⊆ 𝑒 → ( 𝑒 ∖ { ∅ } ) ≼ 𝑒 ) )
93 33 91 92 mpisyl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( 𝑒 ∖ { ∅ } ) ≼ 𝑒 )
94 domtr ⊢ ( ( ( 𝑒 ∖ { ∅ } ) ≼ 𝑒 ∧ 𝑒 ≼ ω ) → ( 𝑒 ∖ { ∅ } ) ≼ ω )
95 93 39 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( 𝑒 ∖ { ∅ } ) ≼ ω )
96 67 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( 𝑒 ∖ { ∅ } ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
97 simprr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Disj 𝑔 ∈ 𝑒 𝑔 )
98 nfcv ⊢ Ⅎ 𝑦 𝑔
99 nfcv ⊢ Ⅎ 𝑔 𝑦
100 id ⊢ ( 𝑔 = 𝑦 → 𝑔 = 𝑦 )
101 98 99 100 cbvdisj ⊢ ( Disj 𝑔 ∈ 𝑒 𝑔 ↔ Disj 𝑦 ∈ 𝑒 𝑦 )
102 97 101 sylib ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Disj 𝑦 ∈ 𝑒 𝑦 )
103 disjss1 ⊢ ( ( 𝑒 ∖ { ∅ } ) ⊆ 𝑒 → ( Disj 𝑦 ∈ 𝑒 𝑦 → Disj 𝑦 ∈ ( 𝑒 ∖ { ∅ } ) 𝑦 ) )
104 91 102 103 mpsyl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Disj 𝑦 ∈ ( 𝑒 ∖ { ∅ } ) 𝑦 )
105 41 42 43 56 90 95 96 104 64 carsggect ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ ( 𝑒 ∖ { ∅ } ) ( 𝑀 ‘ 𝑓 ) ≤ ( 𝑀 ‘ ∪ ( 𝑒 ∖ { ∅ } ) ) )
106 89 105 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ 𝑒 ( 𝑀 ‘ 𝑓 ) ≤ ( 𝑀 ‘ ∪ ( 𝑒 ∖ { ∅ } ) ) )
107 unidif0 ⊢ ∪ ( 𝑒 ∖ { ∅ } ) = ∪ 𝑒
108 107 fveq2i ⊢ ( 𝑀 ‘ ∪ ( 𝑒 ∖ { ∅ } ) ) = ( 𝑀 ‘ ∪ 𝑒 )
109 106 108 breqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ 𝑒 ( 𝑀 ‘ 𝑓 ) ≤ ( 𝑀 ‘ ∪ 𝑒 ) )
110 69 70 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = ( 𝑀 ‘ ∪ 𝑒 ) )
111 109 80 110 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ≤ ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) )
112 81 111 jca ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ≤ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∧ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ≤ ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ) )
113 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
114 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( 𝑀 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
115 114 69 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ∈ ( 0 [,] +∞ ) )
116 113 115 sselid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ∈ ℝ* )
117 114 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → ( 𝑀 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
118 117 76 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) ∧ 𝑓 ∈ 𝑒 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
119 118 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ∀ 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
120 nfcv ⊢ Ⅎ 𝑓 𝑒
121 120 esumcl ⊢ ( ( 𝑒 ∈ 𝒫 𝑆 ∧ ∀ 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
122 33 119 121 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
123 113 122 sselid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ℝ* )
124 xrletri3 ⊢ ( ( ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ∈ ℝ* ∧ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∈ ℝ* ) → ( ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ↔ ( ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ≤ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∧ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ≤ ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ) ) )
125 116 123 124 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ↔ ( ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ≤ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ∧ Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ≤ ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) ) ) )
126 112 125 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑔 ∈ 𝑒 𝑔 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) )
127 30 126 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) ∧ ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) )
128 127 ex ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑆 ) → ( ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ) )
129 128 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑆 ( ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ) )
130 19 25 129 3jca ⊢ ( 𝜑 → ( ( 𝑀 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑀 ↾ 𝑆 ) ‘ ∅ ) = 0 ∧ ∀ 𝑒 ∈ 𝒫 𝑆 ( ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ) ) )
131 16 15 20 54 62 carsgsiga ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ∈ ( sigAlgebra ‘ ∪ 𝑄 ) )
132 2 131 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑄 ) )
133 elrnsiga ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑄 ) → 𝑆 ∈ ∪ ran sigAlgebra )
134 ismeas ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( 𝑀 ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑀 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑀 ↾ 𝑆 ) ‘ ∅ ) = 0 ∧ ∀ 𝑒 ∈ 𝒫 𝑆 ( ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ) ) ) )
135 132 133 134 3syl ⊢ ( 𝜑 → ( ( 𝑀 ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑀 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑀 ↾ 𝑆 ) ‘ ∅ ) = 0 ∧ ∀ 𝑒 ∈ 𝒫 𝑆 ( ( 𝑒 ≼ ω ∧ Disj 𝑓 ∈ 𝑒 𝑓 ) → ( ( 𝑀 ↾ 𝑆 ) ‘ ∪ 𝑒 ) = Σ* 𝑓 ∈ 𝑒 ( ( 𝑀 ↾ 𝑆 ) ‘ 𝑓 ) ) ) ) )
136 130 135 mpbird ⊢ ( 𝜑 → ( 𝑀 ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) )