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 φ x F -1 x +∞ dom vol
Assertion ismbf3d φ F MblFn

Proof

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