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 ⊢ φ → F : A ⟶ ℝ
ismbf2d.2 ⊢ φ → A ∈ dom ⁡ vol
ismbf2d.3 ⊢ φ ∧ x ∈ ℝ → F -1 x +∞ ∈ dom ⁡ vol
ismbf2d.4 ⊢ φ ∧ x ∈ ℝ → F -1 −∞ x ∈ dom ⁡ vol
Assertion ismbf2d ⊢ φ → F ∈ MblFn

Proof

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