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

Metamath Proof Explorer

Theorem mbfdm

Description: The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfdm ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 ref ⊢ ℜ : ℂ ⟶ ℝ
2 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
3 fco ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
4 1 2 3 sylancr ⊢ ( 𝐹 ∈ MblFn → ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
5 fimacnv ⊢ ( ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ → ( ◡ ( ℜ ∘ 𝐹 ) “ ℝ ) = dom 𝐹 )
6 4 5 syl ⊢ ( 𝐹 ∈ MblFn → ( ◡ ( ℜ ∘ 𝐹 ) “ ℝ ) = dom 𝐹 )
7 imaeq2 ⊢ ( 𝑥 = ℝ → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) = ( ◡ ( ℜ ∘ 𝐹 ) “ ℝ ) )
8 7 eleq1d ⊢ ( 𝑥 = ℝ → ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ↔ ( ◡ ( ℜ ∘ 𝐹 ) “ ℝ ) ∈ dom vol ) )
9 ismbf1 ⊢ ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
10 simpl ⊢ ( ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
11 10 ralimi ⊢ ( ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) → ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
12 9 11 simplbiim ⊢ ( 𝐹 ∈ MblFn → ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
13 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
14 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
15 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
16 14 15 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
17 mnfxr ⊢ -∞ ∈ ℝ*
18 pnfxr ⊢ +∞ ∈ ℝ*
19 fnovrn ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -∞ (,) +∞ ) ∈ ran (,) )
20 16 17 18 19 mp3an ⊢ ( -∞ (,) +∞ ) ∈ ran (,)
21 13 20 eqeltrri ⊢ ℝ ∈ ran (,)
22 21 a1i ⊢ ( 𝐹 ∈ MblFn → ℝ ∈ ran (,) )
23 8 12 22 rspcdva ⊢ ( 𝐹 ∈ MblFn → ( ◡ ( ℜ ∘ 𝐹 ) “ ℝ ) ∈ dom vol )
24 6 23 eqeltrrd ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )