Metamath Proof Explorer


Theorem ismbf3d

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

Ref Expression
Hypotheses ismbf3d.1 φF:A
ismbf3d.2 φxF-1x+∞domvol
Assertion ismbf3d φFMblFn

Proof

Step Hyp Ref Expression
1 ismbf3d.1 φF:A
2 ismbf3d.2 φxF-1x+∞domvol
3 fimacnv F:AF-1=A
4 1 3 syl φF-1=A
5 imaiun F-1yy+∞=yF-1y+∞
6 ioossre y+∞
7 6 rgenw yy+∞
8 iunss yy+∞yy+∞
9 7 8 mpbir yy+∞
10 renegcl zz
11 arch zyz<y
12 10 11 syl zyz<y
13 simpl zyz
14 13 biantrurd zyy<zzy<z
15 nnre yy
16 ltnegcon1 zyz<yy<z
17 15 16 sylan2 zyz<yy<z
18 15 adantl zyy
19 18 renegcld zyy
20 19 rexrd zyy*
21 elioopnf y*zy+∞zy<z
22 20 21 syl zyzy+∞zy<z
23 14 17 22 3bitr4d zyz<yzy+∞
24 23 rexbidva zyz<yyzy+∞
25 12 24 mpbid zyzy+∞
26 eliun zyy+∞yzy+∞
27 25 26 sylibr zzyy+∞
28 27 ssriv yy+∞
29 9 28 eqssi yy+∞=
30 29 imaeq2i F-1yy+∞=F-1
31 5 30 eqtr3i yF-1y+∞=F-1
32 2 ralrimiva φxF-1x+∞domvol
33 15 renegcld yy
34 oveq1 x=yx+∞=y+∞
35 34 imaeq2d x=yF-1x+∞=F-1y+∞
36 35 eleq1d x=yF-1x+∞domvolF-1y+∞domvol
37 36 rspccva xF-1x+∞domvolyF-1y+∞domvol
38 32 33 37 syl2an φyF-1y+∞domvol
39 38 ralrimiva φyF-1y+∞domvol
40 iunmbl yF-1y+∞domvolyF-1y+∞domvol
41 39 40 syl φyF-1y+∞domvol
42 31 41 eqeltrrid φF-1domvol
43 4 42 eqeltrrd φAdomvol
44 imaiun F-1y−∞z1y=yF-1−∞z1y
45 eliun xy−∞z1yyx−∞z1y
46 3simpb x−∞<xxz1yxxz1y
47 simplr φzyxz
48 nnrp yy+
49 48 ad2antrl φzyxy+
50 49 rpreccld φzyx1y+
51 47 50 ltsubrpd φzyxz1y<z
52 simprr φzyxx
53 simpr φzz
54 nnrecre y1y
55 resubcl z1yz1y
56 53 54 55 syl2an φzyz1y
57 56 adantrr φzyxz1y
58 lelttr xz1yzxz1yz1y<zx<z
59 52 57 47 58 syl3anc φzyxxz1yz1y<zx<z
60 51 59 mpan2d φzyxxz1yx<z
61 60 anassrs φzyxxz1yx<z
62 61 imdistanda φzyxxz1yxx<z
63 46 62 syl5 φzyx−∞<xxz1yxx<z
64 mnfxr −∞*
65 elioc2 −∞*z1yx−∞z1yx−∞<xxz1y
66 64 56 65 sylancr φzyx−∞z1yx−∞<xxz1y
67 rexr zz*
68 67 adantl φzz*
69 elioomnf z*x−∞zxx<z
70 68 69 syl φzx−∞zxx<z
71 70 adantr φzyx−∞zxx<z
72 63 66 71 3imtr4d φzyx−∞z1yx−∞z
73 72 rexlimdva φzyx−∞z1yx−∞z
74 73 70 sylibd φzyx−∞z1yxx<z
75 simprl φzxx<zx
76 75 adantr φzxx<zy1y<zxx
77 76 mnfltd φzxx<zy1y<zx−∞<x
78 56 ad2ant2r φzxx<zy1y<zxz1y
79 54 ad2antrl φzxx<zy1y<zx1y
80 simplr φzxx<zz
81 80 adantr φzxx<zy1y<zxz
82 simprr φzxx<zy1y<zx1y<zx
83 79 81 76 82 ltsub13d φzxx<zy1y<zxx<z1y
84 76 78 83 ltled φzxx<zy1y<zxxz1y
85 66 ad2ant2r φzxx<zy1y<zxx−∞z1yx−∞<xxz1y
86 76 77 84 85 mpbir3and φzxx<zy1y<zxx−∞z1y
87 80 75 resubcld φzxx<zzx
88 simprr φzxx<zx<z
89 75 80 posdifd φzxx<zx<z0<zx
90 88 89 mpbid φzxx<z0<zx
91 nnrecl zx0<zxy1y<zx
92 87 90 91 syl2anc φzxx<zy1y<zx
93 86 92 reximddv φzxx<zyx−∞z1y
94 93 ex φzxx<zyx−∞z1y
95 74 94 impbid φzyx−∞z1yxx<z
96 95 70 bitr4d φzyx−∞z1yx−∞z
97 45 96 syl5bb φzxy−∞z1yx−∞z
98 97 eqrdv φzy−∞z1y=−∞z
99 98 imaeq2d φzF-1y−∞z1y=F-1−∞z
100 44 99 eqtr3id φzyF-1−∞z1y=F-1−∞z
101 1 ad2antrr φzyF:A
102 ffun F:AFunF
103 funcnvcnv FunFFunF-1-1
104 imadif FunF-1-1F-1z1y+∞=F-1F-1z1y+∞
105 101 102 103 104 4syl φzyF-1z1y+∞=F-1F-1z1y+∞
106 64 a1i φzy−∞*
107 56 rexrd φzyz1y*
108 pnfxr +∞*
109 108 a1i φzy+∞*
110 56 mnfltd φzy−∞<z1y
111 56 ltpnfd φzyz1y<+∞
112 df-ioc .=u*,v*w*|u<wwv
113 df-ioo .=u*,v*w*|u<ww<v
114 xrltnle z1y*x*z1y<x¬xz1y
115 xrlelttr x*z1y*+∞*xz1yz1y<+∞x<+∞
116 xrlttr −∞*z1y*x*−∞<z1yz1y<x−∞<x
117 112 113 114 113 115 116 ixxun −∞*z1y*+∞*−∞<z1yz1y<+∞−∞z1yz1y+∞=−∞+∞
118 106 107 109 110 111 117 syl32anc φzy−∞z1yz1y+∞=−∞+∞
119 uncom −∞z1yz1y+∞=z1y+∞−∞z1y
120 ioomax −∞+∞=
121 118 119 120 3eqtr3g φzyz1y+∞−∞z1y=
122 ioossre z1y+∞
123 incom z1y+∞−∞z1y=−∞z1yz1y+∞
124 112 113 114 ixxdisj −∞*z1y*+∞*−∞z1yz1y+∞=
125 64 108 124 mp3an13 z1y*−∞z1yz1y+∞=
126 107 125 syl φzy−∞z1yz1y+∞=
127 123 126 eqtrid φzyz1y+∞−∞z1y=
128 uneqdifeq z1y+∞z1y+∞−∞z1y=z1y+∞−∞z1y=z1y+∞=−∞z1y
129 122 127 128 sylancr φzyz1y+∞−∞z1y=z1y+∞=−∞z1y
130 121 129 mpbid φzyz1y+∞=−∞z1y
131 130 imaeq2d φzyF-1z1y+∞=F-1−∞z1y
132 105 131 eqtr3d φzyF-1F-1z1y+∞=F-1−∞z1y
133 42 ad2antrr φzyF-1domvol
134 oveq1 x=z1yx+∞=z1y+∞
135 134 imaeq2d x=z1yF-1x+∞=F-1z1y+∞
136 135 eleq1d x=z1yF-1x+∞domvolF-1z1y+∞domvol
137 32 ad2antrr φzyxF-1x+∞domvol
138 136 137 56 rspcdva φzyF-1z1y+∞domvol
139 difmbl F-1domvolF-1z1y+∞domvolF-1F-1z1y+∞domvol
140 133 138 139 syl2anc φzyF-1F-1z1y+∞domvol
141 132 140 eqeltrrd φzyF-1−∞z1ydomvol
142 141 ralrimiva φzyF-1−∞z1ydomvol
143 iunmbl yF-1−∞z1ydomvolyF-1−∞z1ydomvol
144 142 143 syl φzyF-1−∞z1ydomvol
145 100 144 eqeltrrd φzF-1−∞zdomvol
146 145 ralrimiva φzF-1−∞zdomvol
147 oveq2 z=x−∞z=−∞x
148 147 imaeq2d z=xF-1−∞z=F-1−∞x
149 148 eleq1d z=xF-1−∞zdomvolF-1−∞xdomvol
150 149 cbvralvw zF-1−∞zdomvolxF-1−∞xdomvol
151 146 150 sylib φxF-1−∞xdomvol
152 151 r19.21bi φxF-1−∞xdomvol
153 1 43 2 152 ismbf2d φFMblFn