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

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 eqtrdi ⊢ ( ¬ ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ◡ 𝐹 “ ( 𝐵 (,) 𝐶 ) ) = ∅ )
16 0mbl ⊢ ∅ ∈ dom vol
17 15 16 eqeltrdi ⊢ ( ¬ ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ◡ 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )
18 17 adantl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) ∧ ¬ ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )
19 11 18 pm2.61dan ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝐵 (,) 𝐶 ) ) ∈ dom vol )