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 ⊢ φ → F ∈ MblFn
mbfi1flim.2 ⊢ φ → F : A ⟶ ℝ
Assertion mbfi1flim ⊢ φ → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ A n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x

Proof

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