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 eqtrdi 
 |-  ( 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 eqtrdi 
 |-  ( 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 eqtrdi 
 |-  ( 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 eqtrdi 
 |-  ( 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 )