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=\mathrm{dom}vol$$
	smfmbfcex.x	$$⊢\phi \to X\subseteq ℝ$$
	smfmbfcex.n	$$⊢\phi \to \neg X\in S$$
	smfmbfcex.f	$$⊢F=\left(x\in X⟼0\right)$$
Assertion	smfmbfcex	$$⊢\phi \to \left(F\in \mathrm{SMblFn}\left(S\right)\wedge \neg F\in MblFn\right)$$

Proof

Step	Hyp	Ref	Expression
1		smfmbfcex.s	$$⊢S=\mathrm{dom}vol$$
2		smfmbfcex.x	$$⊢\phi \to X\subseteq ℝ$$
3		smfmbfcex.n	$$⊢\phi \to \neg X\in S$$
4		smfmbfcex.f	$$⊢F=\left(x\in X⟼0\right)$$
5		nfv	$$⊢Ⅎx\phi$$
6		dmvolsal	$$⊢\mathrm{dom}vol\in \mathrm{SAlg}$$
7	1 6	eqeltri	$$⊢S\in \mathrm{SAlg}$$
8	7	a1i	$$⊢\phi \to S\in \mathrm{SAlg}$$
9	1	unieqi	$$⊢\bigcup S=\bigcup \mathrm{dom}vol$$
10		unidmvol	$$⊢\bigcup \mathrm{dom}vol=ℝ$$
11	9 10	eqtri	$$⊢\bigcup S=ℝ$$
12	2 11	sseqtrrdi	$$⊢\phi \to X\subseteq \bigcup S$$
13		0red	$$⊢\phi \to 0\in ℝ$$
14	5 8 12 13 4	smfconst	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
15		0red	$$⊢\left(\phi \wedge x\in X\right)\to 0\in ℝ$$
16	4 15	dmmptd	$$⊢\phi \to \mathrm{dom}F=X$$
17	1	eqcomi	$$⊢\mathrm{dom}vol=S$$
18	17	a1i	$$⊢\phi \to \mathrm{dom}vol=S$$
19	16 18	eleq12d	$$⊢\phi \to \left(\mathrm{dom}F\in \mathrm{dom}vol\leftrightarrow X\in S\right)$$
20	3 19	mtbird	$$⊢\phi \to \neg \mathrm{dom}F\in \mathrm{dom}vol$$
21		mbfdm	$$⊢F\in MblFn\to \mathrm{dom}F\in \mathrm{dom}vol$$
22	20 21	nsyl	$$⊢\phi \to \neg F\in MblFn$$
23	14 22	jca	$$⊢\phi \to \left(F\in \mathrm{SMblFn}\left(S\right)\wedge \neg F\in MblFn\right)$$