# 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 )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ x = -oo ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )`
` |-  ( ( ph /\ ( x e. RR \/ x = +oo \/ x = -oo ) ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )`
` |-  ( ( ph /\ x e. RR* ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )`
` |-  ( ph -> F e. MblFn )`