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 )