Metamath Proof Explorer

Theorem ismbf3d

Description: Simplified form of ismbfd . (Contributed by Mario Carneiro, 18-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 ismbf3d.1 
 |-  ( ph -> F : A --> RR )
2 ismbf3d.2 
 |-  ( ( ph /\ x e. RR ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
3 fimacnv 
 |-  ( F : A --> RR -> ( `' F " RR ) = A )
4 1 3 syl 
 |-  ( ph -> ( `' F " RR ) = A )
5 imaiun 
 |-  ( `' F " U_ y e. NN ( -u y (,) +oo ) ) = U_ y e. NN ( `' F " ( -u y (,) +oo ) )
6 ioossre 
 |-  ( -u y (,) +oo ) C_ RR
7 6 rgenw 
 |-  A. y e. NN ( -u y (,) +oo ) C_ RR
8 iunss 
 |-  ( U_ y e. NN ( -u y (,) +oo ) C_ RR <-> A. y e. NN ( -u y (,) +oo ) C_ RR )
9 7 8 mpbir 
 |-  U_ y e. NN ( -u y (,) +oo ) C_ RR
10 renegcl 
 |-  ( z e. RR -> -u z e. RR )
11 arch 
 |-  ( -u z e. RR -> E. y e. NN -u z < y )
12 10 11 syl 
 |-  ( z e. RR -> E. y e. NN -u z < y )
13 simpl 
 |-  ( ( z e. RR /\ y e. NN ) -> z e. RR )
14 13 biantrurd 
 |-  ( ( z e. RR /\ y e. NN ) -> ( -u y < z <-> ( z e. RR /\ -u y < z ) ) )
15 nnre 
 |-  ( y e. NN -> y e. RR )
16 ltnegcon1 
 |-  ( ( z e. RR /\ y e. RR ) -> ( -u z < y <-> -u y < z ) )
17 15 16 sylan2 
 |-  ( ( z e. RR /\ y e. NN ) -> ( -u z < y <-> -u y < z ) )
18 15 adantl 
 |-  ( ( z e. RR /\ y e. NN ) -> y e. RR )
19 18 renegcld 
 |-  ( ( z e. RR /\ y e. NN ) -> -u y e. RR )
20 19 rexrd 
 |-  ( ( z e. RR /\ y e. NN ) -> -u y e. RR* )
21 elioopnf 
 |-  ( -u y e. RR* -> ( z e. ( -u y (,) +oo ) <-> ( z e. RR /\ -u y < z ) ) )
22 20 21 syl 
 |-  ( ( z e. RR /\ y e. NN ) -> ( z e. ( -u y (,) +oo ) <-> ( z e. RR /\ -u y < z ) ) )
23 14 17 22 3bitr4d 
 |-  ( ( z e. RR /\ y e. NN ) -> ( -u z < y <-> z e. ( -u y (,) +oo ) ) )
24 23 rexbidva 
 |-  ( z e. RR -> ( E. y e. NN -u z < y <-> E. y e. NN z e. ( -u y (,) +oo ) ) )
25 12 24 mpbid 
 |-  ( z e. RR -> E. y e. NN z e. ( -u y (,) +oo ) )
26 eliun 
 |-  ( z e. U_ y e. NN ( -u y (,) +oo ) <-> E. y e. NN z e. ( -u y (,) +oo ) )
27 25 26 sylibr 
 |-  ( z e. RR -> z e. U_ y e. NN ( -u y (,) +oo ) )
28 27 ssriv 
 |-  RR C_ U_ y e. NN ( -u y (,) +oo )
29 9 28 eqssi 
 |-  U_ y e. NN ( -u y (,) +oo ) = RR
30 29 imaeq2i 
 |-  ( `' F " U_ y e. NN ( -u y (,) +oo ) ) = ( `' F " RR )
31 5 30 eqtr3i 
 |-  U_ y e. NN ( `' F " ( -u y (,) +oo ) ) = ( `' F " RR )
32 2 ralrimiva 
 |-  ( ph -> A. x e. RR ( `' F " ( x (,) +oo ) ) e. dom vol )
33 15 renegcld 
 |-  ( y e. NN -> -u y e. RR )
34 oveq1 
 |-  ( x = -u y -> ( x (,) +oo ) = ( -u y (,) +oo ) )
35 34 imaeq2d 
 |-  ( x = -u y -> ( `' F " ( x (,) +oo ) ) = ( `' F " ( -u y (,) +oo ) ) )
36 35 eleq1d 
 |-  ( x = -u y -> ( ( `' F " ( x (,) +oo ) ) e. dom vol <-> ( `' F " ( -u y (,) +oo ) ) e. dom vol ) )
37 36 rspccva 
 |-  ( ( A. x e. RR ( `' F " ( x (,) +oo ) ) e. dom vol /\ -u y e. RR ) -> ( `' F " ( -u y (,) +oo ) ) e. dom vol )
38 32 33 37 syl2an 
 |-  ( ( ph /\ y e. NN ) -> ( `' F " ( -u y (,) +oo ) ) e. dom vol )
39 38 ralrimiva 
 |-  ( ph -> A. y e. NN ( `' F " ( -u y (,) +oo ) ) e. dom vol )
40 iunmbl 
 |-  ( A. y e. NN ( `' F " ( -u y (,) +oo ) ) e. dom vol -> U_ y e. NN ( `' F " ( -u y (,) +oo ) ) e. dom vol )
41 39 40 syl 
 |-  ( ph -> U_ y e. NN ( `' F " ( -u y (,) +oo ) ) e. dom vol )
42 31 41 eqeltrrid 
 |-  ( ph -> ( `' F " RR ) e. dom vol )
43 4 42 eqeltrrd 
 |-  ( ph -> A e. dom vol )
44 imaiun 
 |-  ( `' F " U_ y e. NN ( -oo (,] ( z - ( 1 / y ) ) ) ) = U_ y e. NN ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) )
45 eliun 
 |-  ( x e. U_ y e. NN ( -oo (,] ( z - ( 1 / y ) ) ) <-> E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) )
46 3simpb 
 |-  ( ( x e. RR /\ -oo < x /\ x <_ ( z - ( 1 / y ) ) ) -> ( x e. RR /\ x <_ ( z - ( 1 / y ) ) ) )
47 simplr 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> z e. RR )
48 nnrp 
 |-  ( y e. NN -> y e. RR+ )
49 48 ad2antrl 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> y e. RR+ )
50 49 rpreccld 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> ( 1 / y ) e. RR+ )
51 47 50 ltsubrpd 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> ( z - ( 1 / y ) ) < z )
52 simprr 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> x e. RR )
53 simpr 
 |-  ( ( ph /\ z e. RR ) -> z e. RR )
54 nnrecre 
 |-  ( y e. NN -> ( 1 / y ) e. RR )
55 resubcl 
 |-  ( ( z e. RR /\ ( 1 / y ) e. RR ) -> ( z - ( 1 / y ) ) e. RR )
56 53 54 55 syl2an 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( z - ( 1 / y ) ) e. RR )
57 56 adantrr 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> ( z - ( 1 / y ) ) e. RR )
58 lelttr 
 |-  ( ( x e. RR /\ ( z - ( 1 / y ) ) e. RR /\ z e. RR ) -> ( ( x <_ ( z - ( 1 / y ) ) /\ ( z - ( 1 / y ) ) < z ) -> x < z ) )
59 52 57 47 58 syl3anc 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> ( ( x <_ ( z - ( 1 / y ) ) /\ ( z - ( 1 / y ) ) < z ) -> x < z ) )
60 51 59 mpan2d 
 |-  ( ( ( ph /\ z e. RR ) /\ ( y e. NN /\ x e. RR ) ) -> ( x <_ ( z - ( 1 / y ) ) -> x < z ) )
61 60 anassrs 
 |-  ( ( ( ( ph /\ z e. RR ) /\ y e. NN ) /\ x e. RR ) -> ( x <_ ( z - ( 1 / y ) ) -> x < z ) )
62 61 imdistanda 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( x e. RR /\ x <_ ( z - ( 1 / y ) ) ) -> ( x e. RR /\ x < z ) ) )
63 46 62 syl5 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( x e. RR /\ -oo < x /\ x <_ ( z - ( 1 / y ) ) ) -> ( x e. RR /\ x < z ) ) )
64 mnfxr 
 |-  -oo e. RR*
65 elioc2 
 |-  ( ( -oo e. RR* /\ ( z - ( 1 / y ) ) e. RR ) -> ( x e. ( -oo (,] ( z - ( 1 / y ) ) ) <-> ( x e. RR /\ -oo < x /\ x <_ ( z - ( 1 / y ) ) ) ) )
66 64 56 65 sylancr 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( x e. ( -oo (,] ( z - ( 1 / y ) ) ) <-> ( x e. RR /\ -oo < x /\ x <_ ( z - ( 1 / y ) ) ) ) )
67 rexr 
 |-  ( z e. RR -> z e. RR* )
68 67 adantl 
 |-  ( ( ph /\ z e. RR ) -> z e. RR* )
69 elioomnf 
 |-  ( z e. RR* -> ( x e. ( -oo (,) z ) <-> ( x e. RR /\ x < z ) ) )
70 68 69 syl 
 |-  ( ( ph /\ z e. RR ) -> ( x e. ( -oo (,) z ) <-> ( x e. RR /\ x < z ) ) )
71 70 adantr 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( x e. ( -oo (,) z ) <-> ( x e. RR /\ x < z ) ) )
72 63 66 71 3imtr4d 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( x e. ( -oo (,] ( z - ( 1 / y ) ) ) -> x e. ( -oo (,) z ) ) )
73 72 rexlimdva 
 |-  ( ( ph /\ z e. RR ) -> ( E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) -> x e. ( -oo (,) z ) ) )
74 73 70 sylibd 
 |-  ( ( ph /\ z e. RR ) -> ( E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) -> ( x e. RR /\ x < z ) ) )
75 simprl 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> x e. RR )
76 75 adantr 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> x e. RR )
77 76 mnfltd 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> -oo < x )
78 56 ad2ant2r 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> ( z - ( 1 / y ) ) e. RR )
79 54 ad2antrl 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> ( 1 / y ) e. RR )
80 simplr 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> z e. RR )
81 80 adantr 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> z e. RR )
82 simprr 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> ( 1 / y ) < ( z - x ) )
83 79 81 76 82 ltsub13d 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> x < ( z - ( 1 / y ) ) )
84 76 78 83 ltled 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> x <_ ( z - ( 1 / y ) ) )
85 66 ad2ant2r 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> ( x e. ( -oo (,] ( z - ( 1 / y ) ) ) <-> ( x e. RR /\ -oo < x /\ x <_ ( z - ( 1 / y ) ) ) ) )
86 76 77 84 85 mpbir3and 
 |-  ( ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) /\ ( y e. NN /\ ( 1 / y ) < ( z - x ) ) ) -> x e. ( -oo (,] ( z - ( 1 / y ) ) ) )
87 80 75 resubcld 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> ( z - x ) e. RR )
88 simprr 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> x < z )
89 75 80 posdifd 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> ( x < z <-> 0 < ( z - x ) ) )
90 88 89 mpbid 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> 0 < ( z - x ) )
91 nnrecl 
 |-  ( ( ( z - x ) e. RR /\ 0 < ( z - x ) ) -> E. y e. NN ( 1 / y ) < ( z - x ) )
92 87 90 91 syl2anc 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> E. y e. NN ( 1 / y ) < ( z - x ) )
93 86 92 reximddv 
 |-  ( ( ( ph /\ z e. RR ) /\ ( x e. RR /\ x < z ) ) -> E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) )
94 93 ex 
 |-  ( ( ph /\ z e. RR ) -> ( ( x e. RR /\ x < z ) -> E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) ) )
95 74 94 impbid 
 |-  ( ( ph /\ z e. RR ) -> ( E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) <-> ( x e. RR /\ x < z ) ) )
96 95 70 bitr4d 
 |-  ( ( ph /\ z e. RR ) -> ( E. y e. NN x e. ( -oo (,] ( z - ( 1 / y ) ) ) <-> x e. ( -oo (,) z ) ) )
97 45 96 bitrid 
 |-  ( ( ph /\ z e. RR ) -> ( x e. U_ y e. NN ( -oo (,] ( z - ( 1 / y ) ) ) <-> x e. ( -oo (,) z ) ) )
98 97 eqrdv 
 |-  ( ( ph /\ z e. RR ) -> U_ y e. NN ( -oo (,] ( z - ( 1 / y ) ) ) = ( -oo (,) z ) )
99 98 imaeq2d 
 |-  ( ( ph /\ z e. RR ) -> ( `' F " U_ y e. NN ( -oo (,] ( z - ( 1 / y ) ) ) ) = ( `' F " ( -oo (,) z ) ) )
100 44 99 eqtr3id 
 |-  ( ( ph /\ z e. RR ) -> U_ y e. NN ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) = ( `' F " ( -oo (,) z ) ) )
101 1 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> F : A --> RR )
102 ffun 
 |-  ( F : A --> RR -> Fun F )
103 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
104 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( RR \ ( ( z - ( 1 / y ) ) (,) +oo ) ) ) = ( ( `' F " RR ) \ ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) ) )
105 101 102 103 104 4syl 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( `' F " ( RR \ ( ( z - ( 1 / y ) ) (,) +oo ) ) ) = ( ( `' F " RR ) \ ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) ) )
106 64 a1i 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> -oo e. RR* )
107 56 rexrd 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( z - ( 1 / y ) ) e. RR* )
108 pnfxr 
 |-  +oo e. RR*
109 108 a1i 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> +oo e. RR* )
110 56 mnfltd 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> -oo < ( z - ( 1 / y ) ) )
111 56 ltpnfd 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( z - ( 1 / y ) ) < +oo )
112 df-ioc 
 |-  (,] = ( u e. RR* , v e. RR* |-> { w e. RR* | ( u < w /\ w <_ v ) } )
113 df-ioo 
 |-  (,) = ( u e. RR* , v e. RR* |-> { w e. RR* | ( u < w /\ w < v ) } )
114 xrltnle 
 |-  ( ( ( z - ( 1 / y ) ) e. RR* /\ x e. RR* ) -> ( ( z - ( 1 / y ) ) < x <-> -. x <_ ( z - ( 1 / y ) ) ) )
115 xrlelttr 
 |-  ( ( x e. RR* /\ ( z - ( 1 / y ) ) e. RR* /\ +oo e. RR* ) -> ( ( x <_ ( z - ( 1 / y ) ) /\ ( z - ( 1 / y ) ) < +oo ) -> x < +oo ) )
116 xrlttr 
 |-  ( ( -oo e. RR* /\ ( z - ( 1 / y ) ) e. RR* /\ x e. RR* ) -> ( ( -oo < ( z - ( 1 / y ) ) /\ ( z - ( 1 / y ) ) < x ) -> -oo < x ) )
117 112 113 114 113 115 116 ixxun 
 |-  ( ( ( -oo e. RR* /\ ( z - ( 1 / y ) ) e. RR* /\ +oo e. RR* ) /\ ( -oo < ( z - ( 1 / y ) ) /\ ( z - ( 1 / y ) ) < +oo ) ) -> ( ( -oo (,] ( z - ( 1 / y ) ) ) u. ( ( z - ( 1 / y ) ) (,) +oo ) ) = ( -oo (,) +oo ) )
118 106 107 109 110 111 117 syl32anc 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( -oo (,] ( z - ( 1 / y ) ) ) u. ( ( z - ( 1 / y ) ) (,) +oo ) ) = ( -oo (,) +oo ) )
119 uncom 
 |-  ( ( -oo (,] ( z - ( 1 / y ) ) ) u. ( ( z - ( 1 / y ) ) (,) +oo ) ) = ( ( ( z - ( 1 / y ) ) (,) +oo ) u. ( -oo (,] ( z - ( 1 / y ) ) ) )
120 ioomax 
 |-  ( -oo (,) +oo ) = RR
121 118 119 120 3eqtr3g 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( ( z - ( 1 / y ) ) (,) +oo ) u. ( -oo (,] ( z - ( 1 / y ) ) ) ) = RR )
122 ioossre 
 |-  ( ( z - ( 1 / y ) ) (,) +oo ) C_ RR
123 incom 
 |-  ( ( ( z - ( 1 / y ) ) (,) +oo ) i^i ( -oo (,] ( z - ( 1 / y ) ) ) ) = ( ( -oo (,] ( z - ( 1 / y ) ) ) i^i ( ( z - ( 1 / y ) ) (,) +oo ) )
124 112 113 114 ixxdisj 
 |-  ( ( -oo e. RR* /\ ( z - ( 1 / y ) ) e. RR* /\ +oo e. RR* ) -> ( ( -oo (,] ( z - ( 1 / y ) ) ) i^i ( ( z - ( 1 / y ) ) (,) +oo ) ) = (/) )
125 64 108 124 mp3an13 
 |-  ( ( z - ( 1 / y ) ) e. RR* -> ( ( -oo (,] ( z - ( 1 / y ) ) ) i^i ( ( z - ( 1 / y ) ) (,) +oo ) ) = (/) )
126 107 125 syl 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( -oo (,] ( z - ( 1 / y ) ) ) i^i ( ( z - ( 1 / y ) ) (,) +oo ) ) = (/) )
127 123 126 eqtrid 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( ( z - ( 1 / y ) ) (,) +oo ) i^i ( -oo (,] ( z - ( 1 / y ) ) ) ) = (/) )
128 uneqdifeq 
 |-  ( ( ( ( z - ( 1 / y ) ) (,) +oo ) C_ RR /\ ( ( ( z - ( 1 / y ) ) (,) +oo ) i^i ( -oo (,] ( z - ( 1 / y ) ) ) ) = (/) ) -> ( ( ( ( z - ( 1 / y ) ) (,) +oo ) u. ( -oo (,] ( z - ( 1 / y ) ) ) ) = RR <-> ( RR \ ( ( z - ( 1 / y ) ) (,) +oo ) ) = ( -oo (,] ( z - ( 1 / y ) ) ) ) )
129 122 127 128 sylancr 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( ( ( z - ( 1 / y ) ) (,) +oo ) u. ( -oo (,] ( z - ( 1 / y ) ) ) ) = RR <-> ( RR \ ( ( z - ( 1 / y ) ) (,) +oo ) ) = ( -oo (,] ( z - ( 1 / y ) ) ) ) )
130 121 129 mpbid 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( RR \ ( ( z - ( 1 / y ) ) (,) +oo ) ) = ( -oo (,] ( z - ( 1 / y ) ) ) )
131 130 imaeq2d 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( `' F " ( RR \ ( ( z - ( 1 / y ) ) (,) +oo ) ) ) = ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) )
132 105 131 eqtr3d 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( `' F " RR ) \ ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) ) = ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) )
133 42 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( `' F " RR ) e. dom vol )
134 oveq1 
 |-  ( x = ( z - ( 1 / y ) ) -> ( x (,) +oo ) = ( ( z - ( 1 / y ) ) (,) +oo ) )
135 134 imaeq2d 
 |-  ( x = ( z - ( 1 / y ) ) -> ( `' F " ( x (,) +oo ) ) = ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) )
136 135 eleq1d 
 |-  ( x = ( z - ( 1 / y ) ) -> ( ( `' F " ( x (,) +oo ) ) e. dom vol <-> ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) e. dom vol ) )
137 32 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> A. x e. RR ( `' F " ( x (,) +oo ) ) e. dom vol )
138 136 137 56 rspcdva 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) e. dom vol )
139 difmbl 
 |-  ( ( ( `' F " RR ) e. dom vol /\ ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) e. dom vol ) -> ( ( `' F " RR ) \ ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) ) e. dom vol )
140 133 138 139 syl2anc 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( ( `' F " RR ) \ ( `' F " ( ( z - ( 1 / y ) ) (,) +oo ) ) ) e. dom vol )
141 132 140 eqeltrrd 
 |-  ( ( ( ph /\ z e. RR ) /\ y e. NN ) -> ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) e. dom vol )
142 141 ralrimiva 
 |-  ( ( ph /\ z e. RR ) -> A. y e. NN ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) e. dom vol )
143 iunmbl 
 |-  ( A. y e. NN ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) e. dom vol -> U_ y e. NN ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) e. dom vol )
144 142 143 syl 
 |-  ( ( ph /\ z e. RR ) -> U_ y e. NN ( `' F " ( -oo (,] ( z - ( 1 / y ) ) ) ) e. dom vol )
145 100 144 eqeltrrd 
 |-  ( ( ph /\ z e. RR ) -> ( `' F " ( -oo (,) z ) ) e. dom vol )
146 145 ralrimiva 
 |-  ( ph -> A. z e. RR ( `' F " ( -oo (,) z ) ) e. dom vol )
147 oveq2 
 |-  ( z = x -> ( -oo (,) z ) = ( -oo (,) x ) )
148 147 imaeq2d 
 |-  ( z = x -> ( `' F " ( -oo (,) z ) ) = ( `' F " ( -oo (,) x ) ) )
149 148 eleq1d 
 |-  ( z = x -> ( ( `' F " ( -oo (,) z ) ) e. dom vol <-> ( `' F " ( -oo (,) x ) ) e. dom vol ) )
150 149 cbvralvw 
 |-  ( A. z e. RR ( `' F " ( -oo (,) z ) ) e. dom vol <-> A. x e. RR ( `' F " ( -oo (,) x ) ) e. dom vol )
151 146 150 sylib 
 |-  ( ph -> A. x e. RR ( `' F " ( -oo (,) x ) ) e. dom vol )
152 151 r19.21bi 
 |-  ( ( ph /\ x e. RR ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )
153 1 43 2 152 ismbf2d 
 |-  ( ph -> F e. MblFn )