Metamath Proof Explorer


Theorem ismbf2d

Description: Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses ismbf2d.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
ismbf2d.2 ( 𝜑𝐴 ∈ dom vol )
ismbf2d.3 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
ismbf2d.4 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
Assertion ismbf2d ( 𝜑𝐹 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 ismbf2d.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
2 ismbf2d.2 ( 𝜑𝐴 ∈ dom vol )
3 ismbf2d.3 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
4 ismbf2d.4 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
5 elxr ( 𝑥 ∈ ℝ* ↔ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) )
6 oveq1 ( 𝑥 = +∞ → ( 𝑥 (,) +∞ ) = ( +∞ (,) +∞ ) )
7 iooid ( +∞ (,) +∞ ) = ∅
8 6 7 syl6eq ( 𝑥 = +∞ → ( 𝑥 (,) +∞ ) = ∅ )
9 8 imaeq2d ( 𝑥 = +∞ → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) = ( 𝐹 “ ∅ ) )
10 ima0 ( 𝐹 “ ∅ ) = ∅
11 0mbl ∅ ∈ dom vol
12 10 11 eqeltri ( 𝐹 “ ∅ ) ∈ dom vol
13 9 12 eqeltrdi ( 𝑥 = +∞ → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
14 13 adantl ( ( 𝜑𝑥 = +∞ ) → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
15 fimacnv ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 “ ℝ ) = 𝐴 )
16 1 15 syl ( 𝜑 → ( 𝐹 “ ℝ ) = 𝐴 )
17 16 2 eqeltrd ( 𝜑 → ( 𝐹 “ ℝ ) ∈ dom vol )
18 oveq1 ( 𝑥 = -∞ → ( 𝑥 (,) +∞ ) = ( -∞ (,) +∞ ) )
19 ioomax ( -∞ (,) +∞ ) = ℝ
20 18 19 syl6eq ( 𝑥 = -∞ → ( 𝑥 (,) +∞ ) = ℝ )
21 20 imaeq2d ( 𝑥 = -∞ → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) = ( 𝐹 “ ℝ ) )
22 21 eleq1d ( 𝑥 = -∞ → ( ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ↔ ( 𝐹 “ ℝ ) ∈ dom vol ) )
23 17 22 syl5ibrcom ( 𝜑 → ( 𝑥 = -∞ → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ) )
24 23 imp ( ( 𝜑𝑥 = -∞ ) → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
25 3 14 24 3jaodan ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
26 5 25 sylan2b ( ( 𝜑𝑥 ∈ ℝ* ) → ( 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
27 oveq2 ( 𝑥 = +∞ → ( -∞ (,) 𝑥 ) = ( -∞ (,) +∞ ) )
28 27 19 syl6eq ( 𝑥 = +∞ → ( -∞ (,) 𝑥 ) = ℝ )
29 28 imaeq2d ( 𝑥 = +∞ → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) = ( 𝐹 “ ℝ ) )
30 29 eleq1d ( 𝑥 = +∞ → ( ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ↔ ( 𝐹 “ ℝ ) ∈ dom vol ) )
31 17 30 syl5ibrcom ( 𝜑 → ( 𝑥 = +∞ → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ) )
32 31 imp ( ( 𝜑𝑥 = +∞ ) → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
33 oveq2 ( 𝑥 = -∞ → ( -∞ (,) 𝑥 ) = ( -∞ (,) -∞ ) )
34 iooid ( -∞ (,) -∞ ) = ∅
35 33 34 syl6eq ( 𝑥 = -∞ → ( -∞ (,) 𝑥 ) = ∅ )
36 35 imaeq2d ( 𝑥 = -∞ → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) = ( 𝐹 “ ∅ ) )
37 36 12 eqeltrdi ( 𝑥 = -∞ → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
38 37 adantl ( ( 𝜑𝑥 = -∞ ) → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
39 4 32 38 3jaodan ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
40 5 39 sylan2b ( ( 𝜑𝑥 ∈ ℝ* ) → ( 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
41 1 26 40 ismbfd ( 𝜑𝐹 ∈ MblFn )