Metamath Proof Explorer

Theorem mbfi1flim

Description: Any real measurable function has a sequence of simple functions that converges to it. (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses mbfi1flim.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfi1flim.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
Assertion mbfi1flim ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1flim.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfi1flim.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3 iftrue ⊢ ( 𝑦 ∈ 𝐴 → if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) = ( 𝐹 ‘ 𝑦 ) )
4 3 mpteq2ia ⊢ ( 𝑦 ∈ 𝐴 ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) )
5 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
6 5 1 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn )
7 4 6 eqeltrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
8 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
9 c0ex ⊢ 0 ∈ V
10 8 9 ifex ⊢ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ V
11 10 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ V )
12 7 11 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
13 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
14 12 13 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
15 rembl ⊢ ℝ ∈ dom vol
16 15 a1i ⊢ ( 𝜑 → ℝ ∈ dom vol )
17 eldifn ⊢ ( 𝑦 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑦 ∈ 𝐴 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑦 ∈ 𝐴 )
19 18 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) = 0 )
20 14 16 11 19 7 mbfss ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
21 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
22 0red ⊢ ( ( 𝜑 ∧ ¬ 𝑦 ∈ 𝐴 ) → 0 ∈ ℝ )
23 21 22 ifclda ⊢ ( 𝜑 → if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ )
25 24 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) : ℝ ⟶ ℝ )
26 20 25 mbfi1flimlem ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) )
27 ssralv ⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) )
28 14 27 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) )
29 14 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
30 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
31 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
32 30 31 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
33 eqid ⊢ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
34 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
35 34 9 ifex ⊢ if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
36 32 33 35 fvmpt ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
37 29 36 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
38 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
40 37 39 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
41 40 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )
42 41 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )
43 28 42 sylibd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )
44 43 anim2d ⊢ ( 𝜑 → ( ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) )
45 44 eximdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝐴 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) )
46 26 45 mpd ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )