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-1x+∞∈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-1x+∞∈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-1x+∞=F-1∅
10 ima0 ⊢F-1∅=∅
11 0mbl ⊢∅∈dom⁡vol
12 10 11 eqeltri ⊢F-1∅∈dom⁡vol
13 9 12 eqeltrdi ⊢x=+∞→F-1x+∞∈dom⁡vol
14 13 adantl ⊢φ∧x=+∞→F-1x+∞∈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-1x+∞=F-1ℝ
22 21 eleq1d ⊢x=−∞→F-1x+∞∈dom⁡vol↔F-1ℝ∈dom⁡vol
23 17 22 syl5ibrcom ⊢φ→x=−∞→F-1x+∞∈dom⁡vol
24 23 imp ⊢φ∧x=−∞→F-1x+∞∈dom⁡vol
25 3 14 24 3jaodan ⊢φ∧x∈ℝ∨x=+∞∨x=−∞→F-1x+∞∈dom⁡vol
26 5 25 sylan2b ⊢φ∧x∈ℝ*→F-1x+∞∈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