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	|- -. ( SMblFn ` S ) C_ MblFn

Proof

Step	Hyp	Ref	Expression
1		nsssmfmbf.1	|- S = dom vol
2		vitali2	|- dom vol C. ~P RR
3	2	pssnssi	|- -. ~P RR C_ dom vol
4		nss	|- ( -. ~P RR C_ dom vol <-> E. x ( x e. ~P RR /\ -. x e. dom vol ) )
5	3 4	mpbi	|- E. x ( x e. ~P RR /\ -. x e. dom vol )
6		elpwi	|- ( x e. ~P RR -> x C_ RR )
7	6	adantr	|- ( ( x e. ~P RR /\ -. x e. dom vol ) -> x C_ RR )
8	1	eleq2i	|- ( x e. S <-> x e. dom vol )
9	8	bicomi	|- ( x e. dom vol <-> x e. S )
10	9	notbii	|- ( -. x e. dom vol <-> -. x e. S )
11	10	biimpi	|- ( -. x e. dom vol -> -. x e. S )
12	11	adantl	|- ( ( x e. ~P RR /\ -. x e. dom vol ) -> -. x e. S )
13		eqid	|- ( y e. x |-> 0 ) = ( y e. x |-> 0 )
14	1 7 12 13	nsssmfmbflem	|- ( ( x e. ~P RR /\ -. x e. dom vol ) -> E. f ( f e. ( SMblFn ` S ) /\ -. f e. MblFn ) )
15	14	exlimiv	|- ( E. x ( x e. ~P RR /\ -. x e. dom vol ) -> E. f ( f e. ( SMblFn ` S ) /\ -. f e. MblFn ) )
16	5 15	ax-mp	|- E. f ( f e. ( SMblFn ` S ) /\ -. f e. MblFn )
17		nss	|- ( -. ( SMblFn ` S ) C_ MblFn <-> E. f ( f e. ( SMblFn ` S ) /\ -. f e. MblFn ) )
18	16 17	mpbir	|- -. ( SMblFn ` S ) C_ MblFn