Metamath Proof Explorer

Theorem nsssmfmbf

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
	Hypothesis	nsssmfmbf.1	$⊢ S = dom vol$
	Assertion	nsssmfmbf	$⊢ \neg SMblFn (S) \subseteq MblFn$

Proof

Step	Hyp	Ref	Expression
1		nsssmfmbf.1	$⊢ S = dom vol$
2		vitali2	$⊢ dom vol \subset 𝒫 ℝ$
3	2	pssnssi	$⊢ \neg 𝒫 ℝ \subseteq dom vol$
4		nss	$⊢ \neg 𝒫 ℝ \subseteq dom vol \leftrightarrow \exists x (x \in 𝒫 ℝ \land \neg x \in dom vol)$
5	3 4	mpbi	$⊢ \exists x (x \in 𝒫 ℝ \land \neg x \in dom vol)$
6		elpwi	$⊢ x \in 𝒫 ℝ \to x \subseteq ℝ$
7	6	adantr	$⊢ (x \in 𝒫 ℝ \land \neg x \in dom vol) \to x \subseteq ℝ$
8	1	eleq2i	$⊢ x \in S \leftrightarrow x \in dom vol$
9	8	bicomi	$⊢ x \in dom vol \leftrightarrow x \in S$
10	9	notbii	$⊢ \neg x \in dom vol \leftrightarrow \neg x \in S$
11	10	bilani	$⊢ (x \in 𝒫 ℝ \land \neg x \in dom vol) \to \neg x \in S$
12		eqid	$⊢ (y \in x ⟼ 0) = (y \in x ⟼ 0)$
13	1 7 11 12	nsssmfmbflem	$⊢ (x \in 𝒫 ℝ \land \neg x \in dom vol) \to \exists f (f \in SMblFn (S) \land \neg f \in MblFn)$
14	13	exlimiv	$⊢ \exists x (x \in 𝒫 ℝ \land \neg x \in dom vol) \to \exists f (f \in SMblFn (S) \land \neg f \in MblFn)$
15	5 14	ax-mp	$⊢ \exists f (f \in SMblFn (S) \land \neg f \in MblFn)$
16		nss	$⊢ \neg SMblFn (S) \subseteq MblFn \leftrightarrow \exists f (f \in SMblFn (S) \land \neg f \in MblFn)$
17	15 16	mpbir	$⊢ \neg SMblFn (S) \subseteq MblFn$