Metamath Proof Explorer

Theorem ismbfd

Description: Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d . (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses ismbfd.1 
|- ( ph -> F : A --> RR )
ismbfd.2 
|- ( ( ph /\ x e. RR* ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
ismbfd.3 
|- ( ( ph /\ x e. RR* ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
Assertion ismbfd 
|- ( ph -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 ismbfd.1 
 |-  ( ph -> F : A --> RR )
2 ismbfd.2 
 |-  ( ( ph /\ x e. RR* ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
3 ismbfd.3 
 |-  ( ( ph /\ x e. RR* ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
4 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
5 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
6 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( z e. ran (,) <-> E. x e. RR* E. y e. RR* z = ( x (,) y ) ) )
7 4 5 6 mp2b 
 |-  ( z e. ran (,) <-> E. x e. RR* E. y e. RR* z = ( x (,) y ) )
8 simprl 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> x e. RR* )
9 pnfxr 
 |-  +oo e. RR*
10 9 a1i 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> +oo e. RR* )
11 mnfxr 
 |-  -oo e. RR*
12 11 a1i 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> -oo e. RR* )
13 simprr 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> y e. RR* )
14 iooin 
 |-  ( ( ( x e. RR* /\ +oo e. RR* ) /\ ( -oo e. RR* /\ y e. RR* ) ) -> ( ( x (,) +oo ) i^i ( -oo (,) y ) ) = ( if ( x <_ -oo , -oo , x ) (,) if ( +oo <_ y , +oo , y ) ) )
15 8 10 12 13 14 syl22anc 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( ( x (,) +oo ) i^i ( -oo (,) y ) ) = ( if ( x <_ -oo , -oo , x ) (,) if ( +oo <_ y , +oo , y ) ) )
16 ifcl 
 |-  ( ( -oo e. RR* /\ x e. RR* ) -> if ( x <_ -oo , -oo , x ) e. RR* )
17 11 8 16 sylancr 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> if ( x <_ -oo , -oo , x ) e. RR* )
18 mnfle 
 |-  ( x e. RR* -> -oo <_ x )
19 xrleid 
 |-  ( x e. RR* -> x <_ x )
20 breq1 
 |-  ( -oo = if ( x <_ -oo , -oo , x ) -> ( -oo <_ x <-> if ( x <_ -oo , -oo , x ) <_ x ) )
21 breq1 
 |-  ( x = if ( x <_ -oo , -oo , x ) -> ( x <_ x <-> if ( x <_ -oo , -oo , x ) <_ x ) )
22 20 21 ifboth 
 |-  ( ( -oo <_ x /\ x <_ x ) -> if ( x <_ -oo , -oo , x ) <_ x )
23 18 19 22 syl2anc 
 |-  ( x e. RR* -> if ( x <_ -oo , -oo , x ) <_ x )
24 23 ad2antrl 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> if ( x <_ -oo , -oo , x ) <_ x )
25 xrmax1 
 |-  ( ( x e. RR* /\ -oo e. RR* ) -> x <_ if ( x <_ -oo , -oo , x ) )
26 8 11 25 sylancl 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> x <_ if ( x <_ -oo , -oo , x ) )
27 17 8 24 26 xrletrid 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> if ( x <_ -oo , -oo , x ) = x )
28 ifcl 
 |-  ( ( +oo e. RR* /\ y e. RR* ) -> if ( +oo <_ y , +oo , y ) e. RR* )
29 9 13 28 sylancr 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> if ( +oo <_ y , +oo , y ) e. RR* )
30 xrmin2 
 |-  ( ( +oo e. RR* /\ y e. RR* ) -> if ( +oo <_ y , +oo , y ) <_ y )
31 9 13 30 sylancr 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> if ( +oo <_ y , +oo , y ) <_ y )
32 pnfge 
 |-  ( y e. RR* -> y <_ +oo )
33 xrleid 
 |-  ( y e. RR* -> y <_ y )
34 breq2 
 |-  ( +oo = if ( +oo <_ y , +oo , y ) -> ( y <_ +oo <-> y <_ if ( +oo <_ y , +oo , y ) ) )
35 breq2 
 |-  ( y = if ( +oo <_ y , +oo , y ) -> ( y <_ y <-> y <_ if ( +oo <_ y , +oo , y ) ) )
36 34 35 ifboth 
 |-  ( ( y <_ +oo /\ y <_ y ) -> y <_ if ( +oo <_ y , +oo , y ) )
37 32 33 36 syl2anc 
 |-  ( y e. RR* -> y <_ if ( +oo <_ y , +oo , y ) )
38 37 ad2antll 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> y <_ if ( +oo <_ y , +oo , y ) )
39 29 13 31 38 xrletrid 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> if ( +oo <_ y , +oo , y ) = y )
40 27 39 oveq12d 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( if ( x <_ -oo , -oo , x ) (,) if ( +oo <_ y , +oo , y ) ) = ( x (,) y ) )
41 15 40 eqtrd 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( ( x (,) +oo ) i^i ( -oo (,) y ) ) = ( x (,) y ) )
42 41 imaeq2d 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( `' F " ( ( x (,) +oo ) i^i ( -oo (,) y ) ) ) = ( `' F " ( x (,) y ) ) )
43 1 adantr 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> F : A --> RR )
44 43 ffund 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> Fun F )
45 inpreima 
 |-  ( Fun F -> ( `' F " ( ( x (,) +oo ) i^i ( -oo (,) y ) ) ) = ( ( `' F " ( x (,) +oo ) ) i^i ( `' F " ( -oo (,) y ) ) ) )
46 44 45 syl 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( `' F " ( ( x (,) +oo ) i^i ( -oo (,) y ) ) ) = ( ( `' F " ( x (,) +oo ) ) i^i ( `' F " ( -oo (,) y ) ) ) )
47 42 46 eqtr3d 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( `' F " ( x (,) y ) ) = ( ( `' F " ( x (,) +oo ) ) i^i ( `' F " ( -oo (,) y ) ) ) )
48 2 adantrr 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
49 3 ralrimiva 
 |-  ( ph -> A. x e. RR* ( `' F " ( -oo (,) x ) ) e. dom vol )
50 oveq2 
 |-  ( x = y -> ( -oo (,) x ) = ( -oo (,) y ) )
51 50 imaeq2d 
 |-  ( x = y -> ( `' F " ( -oo (,) x ) ) = ( `' F " ( -oo (,) y ) ) )
52 51 eleq1d 
 |-  ( x = y -> ( ( `' F " ( -oo (,) x ) ) e. dom vol <-> ( `' F " ( -oo (,) y ) ) e. dom vol ) )
53 52 rspccva 
 |-  ( ( A. x e. RR* ( `' F " ( -oo (,) x ) ) e. dom vol /\ y e. RR* ) -> ( `' F " ( -oo (,) y ) ) e. dom vol )
54 49 53 sylan 
 |-  ( ( ph /\ y e. RR* ) -> ( `' F " ( -oo (,) y ) ) e. dom vol )
55 54 adantrl 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( `' F " ( -oo (,) y ) ) e. dom vol )
56 inmbl 
 |-  ( ( ( `' F " ( x (,) +oo ) ) e. dom vol /\ ( `' F " ( -oo (,) y ) ) e. dom vol ) -> ( ( `' F " ( x (,) +oo ) ) i^i ( `' F " ( -oo (,) y ) ) ) e. dom vol )
57 48 55 56 syl2anc 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( ( `' F " ( x (,) +oo ) ) i^i ( `' F " ( -oo (,) y ) ) ) e. dom vol )
58 47 57 eqeltrd 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( `' F " ( x (,) y ) ) e. dom vol )
59 imaeq2 
 |-  ( z = ( x (,) y ) -> ( `' F " z ) = ( `' F " ( x (,) y ) ) )
60 59 eleq1d 
 |-  ( z = ( x (,) y ) -> ( ( `' F " z ) e. dom vol <-> ( `' F " ( x (,) y ) ) e. dom vol ) )
61 58 60 syl5ibrcom 
 |-  ( ( ph /\ ( x e. RR* /\ y e. RR* ) ) -> ( z = ( x (,) y ) -> ( `' F " z ) e. dom vol ) )
62 61 rexlimdvva 
 |-  ( ph -> ( E. x e. RR* E. y e. RR* z = ( x (,) y ) -> ( `' F " z ) e. dom vol ) )
63 7 62 syl5bi 
 |-  ( ph -> ( z e. ran (,) -> ( `' F " z ) e. dom vol ) )
64 63 ralrimiv 
 |-  ( ph -> A. z e. ran (,) ( `' F " z ) e. dom vol )
65 ismbf 
 |-  ( F : A --> RR -> ( F e. MblFn <-> A. z e. ran (,) ( `' F " z ) e. dom vol ) )
66 1 65 syl 
 |-  ( ph -> ( F e. MblFn <-> A. z e. ran (,) ( `' F " z ) e. dom vol ) )
67 64 66 mpbird 
 |-  ( ph -> F e. MblFn )