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

Proof

Step Hyp Ref Expression
1 ismbf ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( 𝐹𝑥 ) ∈ dom vol ) )
2 1 biimpac ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ∀ 𝑥 ∈ ran (,) ( 𝐹𝑥 ) ∈ dom vol )
3 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
4 ffn ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
5 3 4 ax-mp (,) Fn ( ℝ* × ℝ* )
6 fnovrn ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 (,) 𝐶 ) ∈ ran (,) )
7 5 6 mp3an1 ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 (,) 𝐶 ) ∈ ran (,) )
8 imaeq2 ( 𝑥 = ( 𝐵 (,) 𝐶 ) → ( 𝐹𝑥 ) = ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) )
9 8 eleq1d ( 𝑥 = ( 𝐵 (,) 𝐶 ) → ( ( 𝐹𝑥 ) ∈ dom vol ↔ ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol ) )
10 9 rspccva ( ( ∀ 𝑥 ∈ ran (,) ( 𝐹𝑥 ) ∈ dom vol ∧ ( 𝐵 (,) 𝐶 ) ∈ ran (,) ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )
11 2 7 10 syl2an ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) ∧ ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )
12 ndmioo ( ¬ ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 (,) 𝐶 ) = ∅ )
13 12 imaeq2d ( ¬ ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) = ( 𝐹 “ ∅ ) )
14 ima0 ( 𝐹 “ ∅ ) = ∅
15 13 14 syl6eq ( ¬ ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) = ∅ )
16 0mbl ∅ ∈ dom vol
17 15 16 eqeltrdi ( ¬ ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )
18 17 adantl ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) ∧ ¬ ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )
19 11 18 pm2.61dan ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )