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
|- ( ph -> F : A --> RR )
ismbf2d.2
|- ( ph -> A e. dom vol )
ismbf2d.3
|- ( ( ph /\ x e. RR ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
ismbf2d.4
|- ( ( ph /\ x e. RR ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
Assertion ismbf2d
|- ( ph -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 ismbf2d.1
 |-  ( ph -> F : A --> RR )
2 ismbf2d.2
 |-  ( ph -> A e. dom vol )
3 ismbf2d.3
 |-  ( ( ph /\ x e. RR ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
4 ismbf2d.4
 |-  ( ( ph /\ x e. RR ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
5 elxr
 |-  ( x e. RR* <-> ( x e. RR \/ x = +oo \/ x = -oo ) )
6 oveq1
 |-  ( x = +oo -> ( x (,) +oo ) = ( +oo (,) +oo ) )
7 iooid
 |-  ( +oo (,) +oo ) = (/)
8 6 7 syl6eq
 |-  ( x = +oo -> ( x (,) +oo ) = (/) )
9 8 imaeq2d
 |-  ( x = +oo -> ( `' F " ( x (,) +oo ) ) = ( `' F " (/) ) )
10 ima0
 |-  ( `' F " (/) ) = (/)
11 0mbl
 |-  (/) e. dom vol
12 10 11 eqeltri
 |-  ( `' F " (/) ) e. dom vol
13 9 12 eqeltrdi
 |-  ( x = +oo -> ( `' F " ( x (,) +oo ) ) e. dom vol )
14 13 adantl
 |-  ( ( ph /\ x = +oo ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
15 fimacnv
 |-  ( F : A --> RR -> ( `' F " RR ) = A )
16 1 15 syl
 |-  ( ph -> ( `' F " RR ) = A )
17 16 2 eqeltrd
 |-  ( ph -> ( `' F " RR ) e. dom vol )
18 oveq1
 |-  ( x = -oo -> ( x (,) +oo ) = ( -oo (,) +oo ) )
19 ioomax
 |-  ( -oo (,) +oo ) = RR
20 18 19 syl6eq
 |-  ( x = -oo -> ( x (,) +oo ) = RR )
21 20 imaeq2d
 |-  ( x = -oo -> ( `' F " ( x (,) +oo ) ) = ( `' F " RR ) )
22 21 eleq1d
 |-  ( x = -oo -> ( ( `' F " ( x (,) +oo ) ) e. dom vol <-> ( `' F " RR ) e. dom vol ) )
23 17 22 syl5ibrcom
 |-  ( ph -> ( x = -oo -> ( `' F " ( x (,) +oo ) ) e. dom vol ) )
24 23 imp
 |-  ( ( ph /\ x = -oo ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
25 3 14 24 3jaodan
 |-  ( ( ph /\ ( x e. RR \/ x = +oo \/ x = -oo ) ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
26 5 25 sylan2b
 |-  ( ( ph /\ x e. RR* ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
27 oveq2
 |-  ( x = +oo -> ( -oo (,) x ) = ( -oo (,) +oo ) )
28 27 19 syl6eq
 |-  ( x = +oo -> ( -oo (,) x ) = RR )
29 28 imaeq2d
 |-  ( x = +oo -> ( `' F " ( -oo (,) x ) ) = ( `' F " RR ) )
30 29 eleq1d
 |-  ( x = +oo -> ( ( `' F " ( -oo (,) x ) ) e. dom vol <-> ( `' F " RR ) e. dom vol ) )
31 17 30 syl5ibrcom
 |-  ( ph -> ( x = +oo -> ( `' F " ( -oo (,) x ) ) e. dom vol ) )
32 31 imp
 |-  ( ( ph /\ x = +oo ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
33 oveq2
 |-  ( x = -oo -> ( -oo (,) x ) = ( -oo (,) -oo ) )
34 iooid
 |-  ( -oo (,) -oo ) = (/)
35 33 34 syl6eq
 |-  ( x = -oo -> ( -oo (,) x ) = (/) )
36 35 imaeq2d
 |-  ( x = -oo -> ( `' F " ( -oo (,) x ) ) = ( `' F " (/) ) )
37 36 12 eqeltrdi
 |-  ( x = -oo -> ( `' F " ( -oo (,) x ) ) e. dom vol )
38 37 adantl
 |-  ( ( ph /\ x = -oo ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
39 4 32 38 3jaodan
 |-  ( ( ph /\ ( x e. RR \/ x = +oo \/ x = -oo ) ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
40 5 39 sylan2b
 |-  ( ( ph /\ x e. RR* ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
41 1 26 40 ismbfd
 |-  ( ph -> F e. MblFn )