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 )