Theorem smfmbfcex

Description: A constant function, with non-lebesgue-measurable domain is a sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) but it is not a measurable functions ( w.r.t. to df-mbf ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfmbfcex.s	|- S = dom vol
	smfmbfcex.x	|- ( ph -> X C_ RR )
	smfmbfcex.n	|- ( ph -> -. X e. S )
	smfmbfcex.f	|- F = ( x e. X |-> 0 )
Assertion	smfmbfcex	|- ( ph -> ( F e. ( SMblFn ` S ) /\ -. F e. MblFn ) )

Proof

Step	Hyp	Ref	Expression
1		smfmbfcex.s	|- S = dom vol
2		smfmbfcex.x	|- ( ph -> X C_ RR )
3		smfmbfcex.n	|- ( ph -> -. X e. S )
4		smfmbfcex.f	|- F = ( x e. X |-> 0 )
5		nfv	|- F/ x ph
6		dmvolsal	|- dom vol e. SAlg
7	1 6	eqeltri	|- S e. SAlg
8	7	a1i	|- ( ph -> S e. SAlg )
9	1	unieqi	|- U. S = U. dom vol
10		unidmvol	|- U. dom vol = RR
11	9 10	eqtri	|- U. S = RR
12	2 11	sseqtrrdi	|- ( ph -> X C_ U. S )
13		0red	|- ( ph -> 0 e. RR )
14	5 8 12 13 4	smfconst	|- ( ph -> F e. ( SMblFn ` S ) )
15		0red	|- ( ( ph /\ x e. X ) -> 0 e. RR )
16	4 15	dmmptd	|- ( ph -> dom F = X )
17	1	eqcomi	|- dom vol = S
18	17	a1i	|- ( ph -> dom vol = S )
19	16 18	eleq12d	|- ( ph -> ( dom F e. dom vol <-> X e. S ) )
20	3 19	mtbird	|- ( ph -> -. dom F e. dom vol )
21		mbfdm	|- ( F e. MblFn -> dom F e. dom vol )
22	20 21	nsyl	|- ( ph -> -. F e. MblFn )
23	14 22	jca	|- ( ph -> ( F e. ( SMblFn ` S ) /\ -. F e. MblFn ) )