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 )