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

Proof

Step	Hyp	Ref	Expression
1		smfmbfcex.s	⊢ 𝑆 = dom vol
2		smfmbfcex.x	⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
3		smfmbfcex.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑆 )
4		smfmbfcex.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ 0 )
5		nfv	⊢ Ⅎ 𝑥 𝜑
6		dmvolsal	⊢ dom vol ∈ SAlg
7	1 6	eqeltri	⊢ 𝑆 ∈ SAlg
8	7	a1i	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
9	1	unieqi	⊢ ∪ 𝑆 = ∪ dom vol
10		unidmvol	⊢ ∪ dom vol = ℝ
11	9 10	eqtri	⊢ ∪ 𝑆 = ℝ
12	2 11	sseqtrrdi	⊢ ( 𝜑 → 𝑋 ⊆ ∪ 𝑆 )
13		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
14	5 8 12 13 4	smfconst	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
15		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ )
16	4 15	dmmptd	⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
17	1	eqcomi	⊢ dom vol = 𝑆
18	17	a1i	⊢ ( 𝜑 → dom vol = 𝑆 )
19	16 18	eleq12d	⊢ ( 𝜑 → ( dom 𝐹 ∈ dom vol ↔ 𝑋 ∈ 𝑆 ) )
20	3 19	mtbird	⊢ ( 𝜑 → ¬ dom 𝐹 ∈ dom vol )
21		mbfdm	⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
22	20 21	nsyl	⊢ ( 𝜑 → ¬ 𝐹 ∈ MblFn )
23	14 22	jca	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ∧ ¬ 𝐹 ∈ MblFn ) )