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	⊢ 𝑆 = dom vol
Assertion	mbfpsssmf	⊢ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊊ ( SMblFn ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mbfpsssmf.1	⊢ 𝑆 = dom vol
2		elinel1	⊢ ( 𝑓 ∈ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) → 𝑓 ∈ MblFn )
3		elinel2	⊢ ( 𝑓 ∈ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) → 𝑓 ∈ ( ℝ ↑pm ℝ ) )
4		elpmrn	⊢ ( 𝑓 ∈ ( ℝ ↑pm ℝ ) → ran 𝑓 ⊆ ℝ )
5	3 4	syl	⊢ ( 𝑓 ∈ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) → ran 𝑓 ⊆ ℝ )
6	2 5 1	mbfresmf	⊢ ( 𝑓 ∈ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) → 𝑓 ∈ ( SMblFn ‘ 𝑆 ) )
7	6	ssriv	⊢ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊆ ( SMblFn ‘ 𝑆 )
8	1	nsssmfmbf	⊢ ¬ ( SMblFn ‘ 𝑆 ) ⊆ MblFn
9	2	ssriv	⊢ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊆ MblFn
10		nsstr	⊢ ( ( ¬ ( SMblFn ‘ 𝑆 ) ⊆ MblFn ∧ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊆ MblFn ) → ¬ ( SMblFn ‘ 𝑆 ) ⊆ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) )
11	8 9 10	mp2an	⊢ ¬ ( SMblFn ‘ 𝑆 ) ⊆ ( MblFn ∩ ( ℝ ↑pm ℝ ) )
12	7 11	pm3.2i	⊢ ( ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊆ ( SMblFn ‘ 𝑆 ) ∧ ¬ ( SMblFn ‘ 𝑆 ) ⊆ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) )
13		dfpss3	⊢ ( ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊊ ( SMblFn ‘ 𝑆 ) ↔ ( ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊆ ( SMblFn ‘ 𝑆 ) ∧ ¬ ( SMblFn ‘ 𝑆 ) ⊆ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ) )
14	12 13	mpbir	⊢ ( MblFn ∩ ( ℝ ↑pm ℝ ) ) ⊊ ( SMblFn ‘ 𝑆 )