Metamath Proof Explorer

Theorem nsssmfmbflem

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
Hypotheses nsssmfmbflem.s ⊢ S = dom ⁡ vol
nsssmfmbflem.x ⊢ φ → X ⊆ ℝ
nsssmfmbflem.n ⊢ φ → ¬ X ∈ S
nsssmfmbflem.f ⊢ F = x ∈ X ⟼ 0
Assertion nsssmfmbflem ⊢ φ → ∃ f f ∈ SMblFn ⁡ S ∧ ¬ f ∈ MblFn

Proof

Step Hyp Ref Expression
1 nsssmfmbflem.s ⊢ S = dom ⁡ vol
2 nsssmfmbflem.x ⊢ φ → X ⊆ ℝ
3 nsssmfmbflem.n ⊢ φ → ¬ X ∈ S
4 nsssmfmbflem.f ⊢ F = x ∈ X ⟼ 0
5 0red ⊢ φ ∧ x ∈ X → 0 ∈ ℝ
6 5 4 fmptd ⊢ φ → F : X ⟶ ℝ
7 reex ⊢ ℝ ∈ V
8 7 a1i ⊢ φ → ℝ ∈ V
9 8 2 ssexd ⊢ φ → X ∈ V
10 6 9 fexd ⊢ φ → F ∈ V
11 1 2 3 4 smfmbfcex ⊢ φ → F ∈ SMblFn ⁡ S ∧ ¬ F ∈ MblFn
12 eleq1 ⊢ f = F → f ∈ SMblFn ⁡ S ↔ F ∈ SMblFn ⁡ S
13 eleq1 ⊢ f = F → f ∈ MblFn ↔ F ∈ MblFn
14 13 notbid ⊢ f = F → ¬ f ∈ MblFn ↔ ¬ F ∈ MblFn
15 12 14 anbi12d ⊢ f = F → f ∈ SMblFn ⁡ S ∧ ¬ f ∈ MblFn ↔ F ∈ SMblFn ⁡ S ∧ ¬ F ∈ MblFn
16 15 spcegv ⊢ F ∈ V → F ∈ SMblFn ⁡ S ∧ ¬ F ∈ MblFn → ∃ f f ∈ SMblFn ⁡ S ∧ ¬ f ∈ MblFn
17 10 11 16 sylc ⊢ φ → ∃ f f ∈ SMblFn ⁡ S ∧ ¬ f ∈ MblFn