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	$⊢ φ \to F \in MblFn$
	mbfresmf.2	$⊢ φ \to ran F \subseteq ℝ$
	mbfresmf.3	$⊢ S = dom vol$
Assertion	mbfresmf	$⊢ φ \to F \in SMblFn (S)$

Proof

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

Metamath Proof Explorer

Theorem mbfresmf

Proof