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	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
	mbfresmf.2	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
	mbfresmf.3	⊢ 𝑆 = dom vol
Assertion	mbfresmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

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