Metamath Proof Explorer

Theorem mbfresmf

Description: A real-valued measurable function is a sigma-measurable function (w.r.t. the Lebesgue measure on the Reals). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses mbfresmf.1 ⊢ φ → F ∈ MblFn
mbfresmf.2 ⊢ φ → ran ⁡ F ⊆ ℝ
mbfresmf.3 ⊢ S = dom ⁡ vol
Assertion mbfresmf ⊢ φ → F ∈ SMblFn ⁡ S

Proof

Step Hyp Ref Expression
1 mbfresmf.1 ⊢ φ → F ∈ MblFn
2 mbfresmf.2 ⊢ φ → ran ⁡ F ⊆ ℝ
3 mbfresmf.3 ⊢ S = dom ⁡ vol
4 nfv ⊢ Ⅎ a φ
5 3 a1i ⊢ φ → S = dom ⁡ vol
6 dmvolsal ⊢ dom ⁡ vol ∈ SAlg
7 6 a1i ⊢ φ → dom ⁡ vol ∈ SAlg
8 5 7 eqeltrd ⊢ φ → S ∈ SAlg
9 mbfdmssre ⊢ F ∈ MblFn → dom ⁡ F ⊆ ℝ
10 1 9 syl ⊢ φ → dom ⁡ F ⊆ ℝ
11 3 unieqi ⊢ ⋃ S = ⋃ dom ⁡ vol
12 unidmvol ⊢ ⋃ dom ⁡ vol = ℝ
13 11 12 eqtri ⊢ ⋃ S = ℝ
14 10 13 sseqtrrdi ⊢ φ → dom ⁡ F ⊆ ⋃ S
15 mbff ⊢ F ∈ MblFn → F : dom ⁡ F ⟶ ℂ
16 ffn ⊢ F : dom ⁡ F ⟶ ℂ → F Fn dom ⁡ F
17 1 15 16 3syl ⊢ φ → F Fn dom ⁡ F
18 17 2 jca ⊢ φ → F Fn dom ⁡ F ∧ ran ⁡ F ⊆ ℝ
19 df-f ⊢ F : dom ⁡ F ⟶ ℝ ↔ F Fn dom ⁡ F ∧ ran ⁡ F ⊆ ℝ
20 18 19 sylibr ⊢ φ → F : dom ⁡ F ⟶ ℝ
21 20 adantr ⊢ φ ∧ a ∈ ℝ → F : dom ⁡ F ⟶ ℝ
22 rexr ⊢ a ∈ ℝ → a ∈ ℝ *
23 22 adantl ⊢ φ ∧ a ∈ ℝ → a ∈ ℝ *
24 21 23 preimaioomnf ⊢ φ ∧ a ∈ ℝ → F -1 −∞ a = x ∈ dom ⁡ F | F ⁡ x < a
25 24 eqcomd ⊢ φ ∧ a ∈ ℝ → x ∈ dom ⁡ F | F ⁡ x < a = F -1 −∞ a
26 6 elexi ⊢ dom ⁡ vol ∈ V
27 3 26 eqeltri ⊢ S ∈ V
28 27 a1i ⊢ φ ∧ a ∈ ℝ → S ∈ V
29 1 dmexd ⊢ φ → dom ⁡ F ∈ V
30 29 adantr ⊢ φ ∧ a ∈ ℝ → dom ⁡ F ∈ V
31 mbfima ⊢ F ∈ MblFn ∧ F : dom ⁡ F ⟶ ℝ → F -1 −∞ a ∈ dom ⁡ vol
32 1 20 31 syl2anc ⊢ φ → F -1 −∞ a ∈ dom ⁡ vol
33 32 5 eleqtrrd ⊢ φ → F -1 −∞ a ∈ S
34 33 adantr ⊢ φ ∧ a ∈ ℝ → F -1 −∞ a ∈ S
35 cnvimass ⊢ F -1 −∞ a ⊆ dom ⁡ F
36 dfss ⊢ F -1 −∞ a ⊆ dom ⁡ F ↔ F -1 −∞ a = F -1 −∞ a ∩ dom ⁡ F
37 36 biimpi ⊢ F -1 −∞ a ⊆ dom ⁡ F → F -1 −∞ a = F -1 −∞ a ∩ dom ⁡ F
38 35 37 ax-mp ⊢ F -1 −∞ a = F -1 −∞ a ∩ dom ⁡ F
39 28 30 34 38 elrestd ⊢ φ ∧ a ∈ ℝ → F -1 −∞ a ∈ S ↾ 𝑡 dom ⁡ F
40 25 39 eqeltrd ⊢ φ ∧ a ∈ ℝ → x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F
41 4 8 14 20 40 issmfd ⊢ φ → F ∈ SMblFn ⁡ S