Metamath Proof Explorer

Theorem mbfima

Description: Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

		Ref	Expression
	Assertion	mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(B, C)] \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		ismbf	$⊢ F : A ⟶ ℝ \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol)$
2	1	biimpac	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to \forall x \in ran (.) F^{-1} [x] \in dom vol$
3		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
4		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
5	3 4	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
6		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land B \in ℝ^{} \land C \in ℝ^{}) \to (B, C) \in ran (.)$
7	5 6	mp3an1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (B, C) \in ran (.)$
8		imaeq2	$⊢ x = (B, C) \to F^{-1} [x] = F^{-1} [(B, C)]$
9	8	eleq1d	$⊢ x = (B, C) \to (F^{-1} [x] \in dom vol \leftrightarrow F^{-1} [(B, C)] \in dom vol)$
10	9	rspccva	$⊢ (\forall x \in ran (.) F^{-1} [x] \in dom vol \land (B, C) \in ran (.)) \to F^{-1} [(B, C)] \in dom vol$
11	2 7 10	syl2an	$⊢ ((F \in MblFn \land F : A ⟶ ℝ) \land (B \in ℝ^{} \land C \in ℝ^{})) \to F^{-1} [(B, C)] \in dom vol$
12		ndmioo	$⊢ \neg (B \in ℝ^{} \land C \in ℝ^{}) \to (B, C) = \emptyset$
13	12	imaeq2d	$⊢ \neg (B \in ℝ^{} \land C \in ℝ^{}) \to F^{-1} [(B, C)] = F^{-1} [\emptyset]$
14		ima0	$⊢ F^{-1} [\emptyset] = \emptyset$
15	13 14	eqtrdi	$⊢ \neg (B \in ℝ^{} \land C \in ℝ^{}) \to F^{-1} [(B, C)] = \emptyset$
16		0mbl	$⊢ \emptyset \in dom vol$
17	15 16	eqeltrdi	$⊢ \neg (B \in ℝ^{} \land C \in ℝ^{}) \to F^{-1} [(B, C)] \in dom vol$
18	17	adantl	$⊢ ((F \in MblFn \land F : A ⟶ ℝ) \land \neg (B \in ℝ^{} \land C \in ℝ^{})) \to F^{-1} [(B, C)] \in dom vol$
19	11 18	pm2.61dan	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(B, C)] \in dom vol$