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	$⊢ φ \to F \in MblFn$
	mbfi1flim.2	$⊢ φ \to F : A ⟶ ℝ$
Assertion	mbfi1flim	$⊢ φ \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall x \in A (n \in ℕ ⟼ g (n) (x)) ⇝ F (x))$

Proof

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

Metamath Proof Explorer

Theorem mbfi1flim

Proof