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 ∈ MblFn ∧ F : A ⟶ ℝ → F -1 B C ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 ismbf ⊢ F : A ⟶ ℝ → F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
2 1 biimpac ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
3 ioof ⊢ . : ℝ * × ℝ * ⟶ 𝒫 ℝ
4 ffn ⊢ . : ℝ * × ℝ * ⟶ 𝒫 ℝ → . Fn ℝ * × ℝ *
5 3 4 ax-mp ⊢ . Fn ℝ * × ℝ *
6 fnovrn ⊢ . Fn ℝ * × ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B C ∈ ran ⁡ .
7 5 6 mp3an1 ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B C ∈ ran ⁡ .
8 imaeq2 ⊢ x = B C → F -1 x = F -1 B C
9 8 eleq1d ⊢ x = B C → F -1 x ∈ dom ⁡ vol ↔ F -1 B C ∈ dom ⁡ vol
10 9 rspccva ⊢ ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol ∧ B C ∈ ran ⁡ . → F -1 B C ∈ dom ⁡ vol
11 2 7 10 syl2an ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ * ∧ C ∈ ℝ * → F -1 B C ∈ dom ⁡ vol
12 ndmioo ⊢ ¬ B ∈ ℝ * ∧ C ∈ ℝ * → B C = ∅
13 12 imaeq2d ⊢ ¬ B ∈ ℝ * ∧ C ∈ ℝ * → F -1 B C = F -1 ∅
14 ima0 ⊢ F -1 ∅ = ∅
15 13 14 eqtrdi ⊢ ¬ B ∈ ℝ * ∧ C ∈ ℝ * → F -1 B C = ∅
16 0mbl ⊢ ∅ ∈ dom ⁡ vol
17 15 16 eqeltrdi ⊢ ¬ B ∈ ℝ * ∧ C ∈ ℝ * → F -1 B C ∈ dom ⁡ vol
18 17 adantl ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ ¬ B ∈ ℝ * ∧ C ∈ ℝ * → F -1 B C ∈ dom ⁡ vol
19 11 18 pm2.61dan ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 B C ∈ dom ⁡ vol