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