This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐵 ∈ ℝ ) → ( ◡ 𝐹 “ { 𝐵 } ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
2 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3 iccid ⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
4 1 2 3 3syl ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
5 4 imaeq2d ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐵 ∈ ℝ ) → ( ◡ 𝐹 “ ( 𝐵 [,] 𝐵 ) ) = ( ◡ 𝐹 “ { 𝐵 } ) )
6 mbfimaicc ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( ◡ 𝐹 “ ( 𝐵 [,] 𝐵 ) ) ∈ dom vol )
7 6 anabsan2 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( ◡ 𝐹 “ ( 𝐵 [,] 𝐵 ) ) ∈ dom vol )
8 7 3impa ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐵 ∈ ℝ ) → ( ◡ 𝐹 “ ( 𝐵 [,] 𝐵 ) ) ∈ dom vol )
9 5 8 eqeltrrd ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐵 ∈ ℝ ) → ( ◡ 𝐹 “ { 𝐵 } ) ∈ dom vol )