Metamath Proof Explorer

Theorem mbfpsssmf

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

		Ref	Expression
	Hypothesis	mbfpsssmf.1	$⊢ S = dom vol$
	Assertion	mbfpsssmf	$⊢ MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subset SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		mbfpsssmf.1	$⊢ S = dom vol$
2		elinel1	$⊢ f \in (MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ)) \to f \in MblFn$
3		elinel2	$⊢ f \in (MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ)) \to f \in (ℝ ↑_{𝑝𝑚} ℝ)$
4		elpmrn	$⊢ f \in (ℝ ↑_{𝑝𝑚} ℝ) \to ran f \subseteq ℝ$
5	3 4	syl	$⊢ f \in (MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ)) \to ran f \subseteq ℝ$
6	2 5 1	mbfresmf	$⊢ f \in (MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ)) \to f \in SMblFn (S)$
7	6	ssriv	$⊢ MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subseteq SMblFn (S)$
8	1	nsssmfmbf	$⊢ \neg SMblFn (S) \subseteq MblFn$
9	2	ssriv	$⊢ MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subseteq MblFn$
10		nsstr	$⊢ (\neg SMblFn (S) \subseteq MblFn \land MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subseteq MblFn) \to \neg SMblFn (S) \subseteq MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ)$
11	8 9 10	mp2an	$⊢ \neg SMblFn (S) \subseteq MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ)$
12	7 11	pm3.2i	$⊢ (MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subseteq SMblFn (S) \land \neg SMblFn (S) \subseteq MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ))$
13		dfpss3	$⊢ MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subset SMblFn (S) \leftrightarrow (MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subseteq SMblFn (S) \land \neg SMblFn (S) \subseteq MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ))$
14	12 13	mpbir	$⊢ MblFn \cap (ℝ ↑_{𝑝𝑚} ℝ) \subset SMblFn (S)$