Metamath Proof Explorer


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 φ X
smfmbfcex.n φ ¬ X S
smfmbfcex.f F = x X 0
Assertion smfmbfcex φ F SMblFn S ¬ F MblFn

Proof

Step Hyp Ref Expression
1 smfmbfcex.s S = dom vol
2 smfmbfcex.x φ X
3 smfmbfcex.n φ ¬ X S
4 smfmbfcex.f F = x X 0
5 nfv x φ
6 dmvolsal dom vol SAlg
7 1 6 eqeltri S SAlg
8 7 a1i φ S SAlg
9 1 unieqi S = dom vol
10 unidmvol dom vol =
11 9 10 eqtri S =
12 2 11 sseqtrrdi φ X S
13 0red φ 0
14 5 8 12 13 4 smfconst φ F SMblFn S
15 0red φ x X 0
16 4 15 dmmptd φ dom F = X
17 1 eqcomi dom vol = S
18 17 a1i φ dom vol = S
19 16 18 eleq12d φ dom F dom vol X S
20 3 19 mtbird φ ¬ dom F dom vol
21 mbfdm F MblFn dom F dom vol
22 20 21 nsyl φ ¬ F MblFn
23 14 22 jca φ F SMblFn S ¬ F MblFn