mbfdm

Description: The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

		Ref	Expression
	Assertion	mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		ref	$⊢ ℜ : ℂ ⟶ ℝ$
2		mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$
3		fco	$⊢ (ℜ : ℂ ⟶ ℝ \land F : dom F ⟶ ℂ) \to (ℜ \circ F) : dom F ⟶ ℝ$
4	1 2 3	sylancr	$⊢ F \in MblFn \to (ℜ \circ F) : dom F ⟶ ℝ$
5		fimacnv	$⊢ (ℜ \circ F) : dom F ⟶ ℝ \to {(ℜ \circ F)}^{-1} [ℝ] = dom F$
6	4 5	syl	$⊢ F \in MblFn \to {(ℜ \circ F)}^{-1} [ℝ] = dom F$
7		imaeq2	$⊢ x = ℝ \to {(ℜ \circ F)}^{-1} [x] = {(ℜ \circ F)}^{-1} [ℝ]$
8	7	eleq1d	$⊢ x = ℝ \to ({(ℜ \circ F)}^{-1} [x] \in dom vol \leftrightarrow {(ℜ \circ F)}^{-1} [ℝ] \in dom vol)$
9		ismbf1	$⊢ F \in MblFn \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
10		simpl	$⊢ ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol) \to {(ℜ \circ F)}^{-1} [x] \in dom vol$
11	10	ralimi	$⊢ \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol) \to \forall x \in ran (.) {(ℜ \circ F)}^{-1} [x] \in dom vol$
12	9 11	simplbiim	$⊢ F \in MblFn \to \forall x \in ran (.) {(ℜ \circ F)}^{-1} [x] \in dom vol$
13		ioomax	$⊢ (−∞, +∞) = ℝ$
14		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
15		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
16	14 15	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
17		mnfxr	$⊢ −∞ \in ℝ^{*}$
18		pnfxr	$⊢ +∞ \in ℝ^{*}$
19		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land −∞ \in ℝ^{} \land +∞ \in ℝ^{}) \to (−∞, +∞) \in ran (.)$
20	16 17 18 19	mp3an	$⊢ (−∞, +∞) \in ran (.)$
21	13 20	eqeltrri	$⊢ ℝ \in ran (.)$
22	21	a1i	$⊢ F \in MblFn \to ℝ \in ran (.)$
23	8 12 22	rspcdva	$⊢ F \in MblFn \to {(ℜ \circ F)}^{-1} [ℝ] \in dom vol$
24	6 23	eqeltrrd	$⊢ F \in MblFn \to dom F \in dom vol$

Metamath Proof Explorer

Theorem mbfdm

Proof