Metamath Proof Explorer

Theorem mbfi1fseq

Description: A characterization of measurability in terms of simple functions (this is an if and only if for nonnegative functions, although we don't prove it). Any nonnegative measurable function is the limit of an increasing sequence of nonnegative simple functions. This proof is an example of a poor de Bruijn factor - the formalized proof is much longer than an average hand proof, which usually just describes the function G and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfi1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
Assertion mbfi1fseq ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfi1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 2 ↑ 𝑗 ) = ( 2 ↑ 𝑘 ) )
4 3 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) )
5 4 fveq2d ⊢ ( 𝑗 = 𝑘 → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) )
6 5 3 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) )
7 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
8 7 fvoveq1d ⊢ ( 𝑧 = 𝑦 → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑘 ) ) ) )
9 8 oveq1d ⊢ ( 𝑧 = 𝑦 → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) )
10 6 9 cbvmpov ⊢ ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) = ( 𝑘 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) )
11 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) ↔ 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) ) )
12 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) = ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) )
13 12 breq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 ↔ ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 ) )
14 13 12 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) = if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) )
15 11 14 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) = if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) )
16 15 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) )
17 negeq ⊢ ( 𝑚 = 𝑘 → - 𝑚 = - 𝑘 )
18 id ⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 )
19 17 18 oveq12d ⊢ ( 𝑚 = 𝑘 → ( - 𝑚 [,] 𝑚 ) = ( - 𝑘 [,] 𝑘 ) )
20 19 eleq2d ⊢ ( 𝑚 = 𝑘 → ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) ↔ 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) ) )
21 oveq1 ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) = ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) )
22 21 18 breq12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 ↔ ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 ) )
23 22 21 18 ifbieq12d ⊢ ( 𝑚 = 𝑘 → if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) = if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) )
24 20 23 ifbieq1d ⊢ ( 𝑚 = 𝑘 → if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) = if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) )
25 24 mpteq2dv ⊢ ( 𝑚 = 𝑘 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) )
26 16 25 syl5eq ⊢ ( 𝑚 = 𝑘 → ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) )
27 26 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) )
28 1 2 10 27 mbfi1fseqlem6 ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )