Metamath Proof Explorer

Theorem caratheodory

Description: Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caratheodory.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caratheodory.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion caratheodory ( 𝜑 → ( 𝑂 ↾ 𝑆 ) ∈ Meas )

Proof

Step Hyp Ref Expression
1 caratheodory.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 caratheodory.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 1 2 caragensal ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 eqid ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
5 1 4 omef ⊢ ( 𝜑 → 𝑂 : 𝒫 ∪ dom 𝑂 ⟶ ( 0 [,] +∞ ) )
6 caragenval ⊢ ( 𝑂 ∈ OutMeas → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
7 1 6 syl ⊢ ( 𝜑 → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
8 7 eqcomd ⊢ ( 𝜑 → { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } = ( CaraGen ‘ 𝑂 ) )
9 2 eqcomi ⊢ ( CaraGen ‘ 𝑂 ) = 𝑆
10 9 a1i ⊢ ( 𝜑 → ( CaraGen ‘ 𝑂 ) = 𝑆 )
11 8 10 eqtr2d ⊢ ( 𝜑 → 𝑆 = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
12 ssrab2 ⊢ { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ⊆ 𝒫 ∪ dom 𝑂
13 11 12 eqsstrdi ⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 ∪ dom 𝑂 )
14 5 13 fssresd ⊢ ( 𝜑 → ( 𝑂 ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
15 1 2 caragen0 ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
16 fvres ⊢ ( ∅ ∈ 𝑆 → ( ( 𝑂 ↾ 𝑆 ) ‘ ∅ ) = ( 𝑂 ‘ ∅ ) )
17 15 16 syl ⊢ ( 𝜑 → ( ( 𝑂 ↾ 𝑆 ) ‘ ∅ ) = ( 𝑂 ‘ ∅ ) )
18 1 ome0 ⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
19 17 18 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ↾ 𝑆 ) ‘ ∅ ) = 0 )
20 simp1 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝜑 )
21 simp2 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝑒 : ℕ ⟶ 𝑆 )
22 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑒 ‘ 𝑛 ) = ( 𝑒 ‘ 𝑚 ) )
23 22 cbvdisjv ⊢ ( Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ↔ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) )
24 23 biimpi ⊢ ( Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) → Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) )
25 24 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) )
26 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → 𝑂 ∈ OutMeas )
27 simp2 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → 𝑒 : ℕ ⟶ 𝑆 )
28 23 biimpri ⊢ ( Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
29 28 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
30 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑒 ‘ 𝑚 ) = ( 𝑒 ‘ 𝑛 ) )
31 30 cbviunv ⊢ ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝑒 ‘ 𝑚 ) = ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝑒 ‘ 𝑛 )
32 31 mpteq2i ⊢ ( 𝑗 ∈ ℕ ↦ ∪ 𝑚 ∈ ( 1 ... 𝑗 ) ( 𝑒 ‘ 𝑚 ) ) = ( 𝑗 ∈ ℕ ↦ ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝑒 ‘ 𝑛 ) )
33 26 4 2 27 29 32 caratheodorylem2 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
34 20 21 25 33 syl3anc ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
35 3 adantr ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → 𝑆 ∈ SAlg )
36 nnenom ⊢ ℕ ≈ ω
37 endom ⊢ ( ℕ ≈ ω → ℕ ≼ ω )
38 36 37 ax-mp ⊢ ℕ ≼ ω
39 38 a1i ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ℕ ≼ ω )
40 ffvelrn ⊢ ( ( 𝑒 : ℕ ⟶ 𝑆 ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
41 40 adantll ⊢ ( ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
42 35 39 41 saliuncl ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
43 fvres ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 → ( ( 𝑂 ↾ 𝑆 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ( ( 𝑂 ↾ 𝑆 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
45 44 3adant3 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( ( 𝑂 ↾ 𝑆 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
46 fvres ⊢ ( ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 → ( ( 𝑂 ↾ 𝑆 ) ‘ ( 𝑒 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) )
47 41 46 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑂 ↾ 𝑆 ) ‘ ( 𝑒 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) )
48 47 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑂 ↾ 𝑆 ) ‘ ( 𝑒 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) ) )
49 48 fveq2d ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( 𝑂 ↾ 𝑆 ) ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
50 49 3adant3 ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( 𝑂 ↾ 𝑆 ) ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
51 34 45 50 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( ( 𝑂 ↾ 𝑆 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( 𝑂 ↾ 𝑆 ) ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
52 3 14 19 51 ismeannd ⊢ ( 𝜑 → ( 𝑂 ↾ 𝑆 ) ∈ Meas )