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	⊢ 𝑆 = dom vol
	nsssmfmbflem.x	⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
	nsssmfmbflem.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑆 )
	nsssmfmbflem.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ 0 )
Assertion	nsssmfmbflem	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) )

Proof

Step	Hyp	Ref	Expression
1		nsssmfmbflem.s	⊢ 𝑆 = dom vol
2		nsssmfmbflem.x	⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
3		nsssmfmbflem.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑆 )
4		nsssmfmbflem.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ 0 )
5		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ )
6	5 4	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
7		reex	⊢ ℝ ∈ V
8	7	a1i	⊢ ( 𝜑 → ℝ ∈ V )
9	8 2	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
10	6 9	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
11	1 2 3 4	smfmbfcex	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝐹 ∈ MblFn ) )
12		eleq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ↔ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) )
13		eleq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn ) )
14	13	notbid	⊢ ( 𝑓 = 𝐹 → ( ¬ 𝑓 ∈ MblFn ↔ ¬ 𝐹 ∈ MblFn ) )
15	12 14	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) ↔ ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝐹 ∈ MblFn ) ) )
16	15	spcegv	⊢ ( 𝐹 ∈ V → ( ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝐹 ∈ MblFn ) → ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) ) )
17	10 11 16	sylc	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) )