Metamath Proof Explorer

Theorem mbfimasn

Description: The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfimasn ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → F -1 B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 simp3 ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → B ∈ ℝ
2 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
3 iccid ⊢ B ∈ ℝ * → B B = B
4 1 2 3 3syl ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → B B = B
5 4 imaeq2d ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → F -1 B B = F -1 B
6 mbfimaicc ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ B ∈ ℝ → F -1 B B ∈ dom ⁡ vol
7 6 anabsan2 ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → F -1 B B ∈ dom ⁡ vol
8 7 3impa ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → F -1 B B ∈ dom ⁡ vol
9 5 8 eqeltrrd ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ → F -1 B ∈ dom ⁡ vol