Metamath Proof Explorer

Theorem nsssmfmbflem

Description: The sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) are not a subset of the measurable functions. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypotheses	nsssmfmbflem.s	$⊢ S = dom vol$
		nsssmfmbflem.x	$⊢ φ \to X \subseteq ℝ$
		nsssmfmbflem.n	$⊢ φ \to \neg X \in S$
		nsssmfmbflem.f	$⊢ F = (x \in X ⟼ 0)$
	Assertion	nsssmfmbflem	$⊢ φ \to \exists f (f \in SMblFn (S) \land \neg f \in MblFn)$

Proof

Step	Hyp	Ref	Expression
1		nsssmfmbflem.s	$⊢ S = dom vol$
2		nsssmfmbflem.x	$⊢ φ \to X \subseteq ℝ$
3		nsssmfmbflem.n	$⊢ φ \to \neg X \in S$
4		nsssmfmbflem.f	$⊢ F = (x \in X ⟼ 0)$
5		0red	$⊢ (φ \land x \in X) \to 0 \in ℝ$
6	5 4	fmptd	$⊢ φ \to F : X ⟶ ℝ$
7		reex	$⊢ ℝ \in V$
8	7	a1i	$⊢ φ \to ℝ \in V$
9	8 2	ssexd	$⊢ φ \to X \in V$
10	6 9	fexd	$⊢ φ \to F \in V$
11	1 2 3 4	smfmbfcex	$⊢ φ \to (F \in SMblFn (S) \land \neg F \in MblFn)$
12		eleq1	$⊢ f = F \to (f \in SMblFn (S) \leftrightarrow F \in SMblFn (S))$
13		eleq1	$⊢ f = F \to (f \in MblFn \leftrightarrow F \in MblFn)$
14	13	notbid	$⊢ f = F \to (\neg f \in MblFn \leftrightarrow \neg F \in MblFn)$
15	12 14	anbi12d	$⊢ f = F \to ((f \in SMblFn (S) \land \neg f \in MblFn) \leftrightarrow (F \in SMblFn (S) \land \neg F \in MblFn))$
16	15	spcegv	$⊢ F \in V \to ((F \in SMblFn (S) \land \neg F \in MblFn) \to \exists f (f \in SMblFn (S) \land \neg f \in MblFn))$
17	10 11 16	sylc	$⊢ φ \to \exists f (f \in SMblFn (S) \land \neg f \in MblFn)$