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	⊢ 𝑆 = dom vol
Assertion	nsssmfmbf	⊢ ¬ ( SMblFn ‘ 𝑆 ) ⊆ MblFn

Proof

Step	Hyp	Ref	Expression
1		nsssmfmbf.1	⊢ 𝑆 = dom vol
2		vitali2	⊢ dom vol ⊊ 𝒫 ℝ
3	2	pssnssi	⊢ ¬ 𝒫 ℝ ⊆ dom vol
4		nss	⊢ ( ¬ 𝒫 ℝ ⊆ dom vol ↔ ∃ 𝑥 ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ 𝑥 ∈ dom vol ) )
5	3 4	mpbi	⊢ ∃ 𝑥 ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ 𝑥 ∈ dom vol )
6		elpwi	⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
7	6	adantr	⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ 𝑥 ∈ dom vol ) → 𝑥 ⊆ ℝ )
8	1	eleq2i	⊢ ( 𝑥 ∈ 𝑆 ↔ 𝑥 ∈ dom vol )
9	8	bicomi	⊢ ( 𝑥 ∈ dom vol ↔ 𝑥 ∈ 𝑆 )
10	9	notbii	⊢ ( ¬ 𝑥 ∈ dom vol ↔ ¬ 𝑥 ∈ 𝑆 )
11	10	biimpi	⊢ ( ¬ 𝑥 ∈ dom vol → ¬ 𝑥 ∈ 𝑆 )
12	11	adantl	⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ 𝑥 ∈ dom vol ) → ¬ 𝑥 ∈ 𝑆 )
13		eqid	⊢ ( 𝑦 ∈ 𝑥 ↦ 0 ) = ( 𝑦 ∈ 𝑥 ↦ 0 )
14	1 7 12 13	nsssmfmbflem	⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ 𝑥 ∈ dom vol ) → ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) )
15	14	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ 𝑥 ∈ dom vol ) → ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) )
16	5 15	ax-mp	⊢ ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn )
17		nss	⊢ ( ¬ ( SMblFn ‘ 𝑆 ) ⊆ MblFn ↔ ∃ 𝑓 ( 𝑓 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝑓 ∈ MblFn ) )
18	16 17	mpbir	⊢ ¬ ( SMblFn ‘ 𝑆 ) ⊆ MblFn