Step |
Hyp |
Ref |
Expression |
1 |
|
hoidmvlelem4.l |
|
2 |
|
hoidmvlelem4.x |
|
3 |
|
hoidmvlelem4.y |
|
4 |
|
hoidmvlelem4.n |
|
5 |
|
hoidmvlelem4.z |
|
6 |
|
hoidmvlelem4.w |
|
7 |
|
hoidmvlelem4.a |
|
8 |
|
hoidmvlelem4.b |
|
9 |
|
hoidmvlelem4.k |
|
10 |
|
hoidmvlelem4.c |
|
11 |
|
hoidmvlelem4.d |
|
12 |
|
hoidmvlelem4.r |
|
13 |
|
hoidmvlelem4.h |
|
14 |
|
hoidmvlelem4.14 |
|
15 |
|
hoidmvlelem4.e |
|
16 |
|
hoidmvlelem4.u |
|
17 |
|
hoidmvlelem4.s |
|
18 |
|
hoidmvlelem4.i |
|
19 |
|
hoidmvlelem4.i2 |
|
20 |
|
rge0ssre |
|
21 |
5
|
eldifad |
|
22 |
|
snssi |
|
23 |
21 22
|
syl |
|
24 |
3 23
|
unssd |
|
25 |
6 24
|
eqsstrid |
|
26 |
|
ssfi |
|
27 |
2 25 26
|
syl2anc |
|
28 |
1 27 7 8
|
hoidmvcl |
|
29 |
20 28
|
sseldi |
|
30 |
|
1red |
|
31 |
15
|
rpred |
|
32 |
30 31
|
readdcld |
|
33 |
|
nfv |
|
34 |
|
nnex |
|
35 |
34
|
a1i |
|
36 |
|
icossicc |
|
37 |
27
|
adantr |
|
38 |
10
|
ffvelrnda |
|
39 |
|
elmapi |
|
40 |
38 39
|
syl |
|
41 |
|
eleq1 |
|
42 |
|
fveq2 |
|
43 |
42
|
breq1d |
|
44 |
43 42
|
ifbieq1d |
|
45 |
41 42 44
|
ifbieq12d |
|
46 |
45
|
cbvmptv |
|
47 |
46
|
mpteq2i |
|
48 |
47
|
mpteq2i |
|
49 |
13 48
|
eqtri |
|
50 |
|
snidg |
|
51 |
5 50
|
syl |
|
52 |
|
elun2 |
|
53 |
51 52
|
syl |
|
54 |
6
|
a1i |
|
55 |
54
|
eqcomd |
|
56 |
53 55
|
eleqtrd |
|
57 |
8 56
|
ffvelrnd |
|
58 |
57
|
adantr |
|
59 |
11
|
ffvelrnda |
|
60 |
|
elmapi |
|
61 |
59 60
|
syl |
|
62 |
49 58 37 61
|
hsphoif |
|
63 |
1 37 40 62
|
hoidmvcl |
|
64 |
36 63
|
sseldi |
|
65 |
33 35 64
|
sge0clmpt |
|
66 |
33 35 64
|
sge0xrclmpt |
|
67 |
|
pnfxr |
|
68 |
67
|
a1i |
|
69 |
12
|
rexrd |
|
70 |
1 37 40 61
|
hoidmvcl |
|
71 |
36 70
|
sseldi |
|
72 |
5
|
eldifbd |
|
73 |
56 72
|
eldifd |
|
74 |
73
|
adantr |
|
75 |
1 37 74 6 58 49 40 61
|
hsphoidmvle |
|
76 |
33 35 64 71 75
|
sge0lempt |
|
77 |
12
|
ltpnfd |
|
78 |
66 69 68 76 77
|
xrlelttrd |
|
79 |
66 68 78
|
xrltned |
|
80 |
|
ge0xrre |
|
81 |
65 79 80
|
syl2anc |
|
82 |
32 81
|
remulcld |
|
83 |
32 12
|
remulcld |
|
84 |
56
|
ancli |
|
85 |
|
eleq1 |
|
86 |
85
|
anbi2d |
|
87 |
|
fveq2 |
|
88 |
|
fveq2 |
|
89 |
87 88
|
breq12d |
|
90 |
86 89
|
imbi12d |
|
91 |
90 9
|
vtoclg |
|
92 |
56 84 91
|
sylc |
|
93 |
1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92
|
hoidmvlelem1 |
|
94 |
57
|
rexrd |
|
95 |
|
iccssxr |
|
96 |
|
ssrab2 |
|
97 |
16 96
|
eqsstri |
|
98 |
97 93
|
sseldi |
|
99 |
95 98
|
sseldi |
|
100 |
|
simpl |
|
101 |
|
simpr |
|
102 |
7 56
|
ffvelrnd |
|
103 |
102 57
|
iccssred |
|
104 |
103 98
|
sseldd |
|
105 |
104
|
adantr |
|
106 |
100 57
|
syl |
|
107 |
105 106
|
ltnled |
|
108 |
101 107
|
mpbird |
|
109 |
2
|
adantr |
|
110 |
3
|
adantr |
|
111 |
5
|
adantr |
|
112 |
7
|
adantr |
|
113 |
8
|
adantr |
|
114 |
9
|
adantlr |
|
115 |
|
eqid |
|
116 |
10
|
adantr |
|
117 |
|
fveq2 |
|
118 |
117
|
fveq1d |
|
119 |
|
fveq2 |
|
120 |
119
|
fveq1d |
|
121 |
118 120
|
oveq12d |
|
122 |
121
|
eleq2d |
|
123 |
117
|
reseq1d |
|
124 |
122 123
|
ifbieq1d |
|
125 |
124
|
cbvmptv |
|
126 |
11
|
adantr |
|
127 |
119
|
reseq1d |
|
128 |
122 127
|
ifbieq1d |
|
129 |
128
|
cbvmptv |
|
130 |
12
|
adantr |
|
131 |
15
|
adantr |
|
132 |
93
|
adantr |
|
133 |
|
simpr |
|
134 |
|
biid |
|
135 |
|
eqidd |
|
136 |
135
|
cbvmptv |
|
137 |
134 136
|
ifbieq2i |
|
138 |
137
|
mpteq2i |
|
139 |
138
|
a1i |
|
140 |
|
id |
|
141 |
139 140
|
fveq12d |
|
142 |
134 136
|
ifbieq2i |
|
143 |
142
|
mpteq2i |
|
144 |
143
|
a1i |
|
145 |
144 140
|
fveq12d |
|
146 |
141 145
|
oveq12d |
|
147 |
146
|
cbvmptv |
|
148 |
18
|
adantr |
|
149 |
19
|
adantr |
|
150 |
|
eqid |
|
151 |
|
fveq2 |
|
152 |
|
fveq2 |
|
153 |
151 152
|
oveq12d |
|
154 |
153
|
cbvixpv |
|
155 |
|
eleq1 |
|
156 |
|
fveq2 |
|
157 |
155 156
|
ifbieq1d |
|
158 |
157
|
cbvmptv |
|
159 |
154 158
|
mpteq12i |
|
160 |
150 159
|
eqtri |
|
161 |
1 109 110 111 6 112 113 114 115 116 125 126 129 130 13 14 131 16 132 133 147 148 149 160
|
hoidmvlelem3 |
|
162 |
100 108 161
|
syl2anc |
|
163 |
97
|
a1i |
|
164 |
163 103
|
sstrd |
|
165 |
164
|
adantr |
|
166 |
|
ne0i |
|
167 |
166
|
adantl |
|
168 |
102
|
rexrd |
|
169 |
168
|
adantr |
|
170 |
94
|
adantr |
|
171 |
163
|
sselda |
|
172 |
|
iccleub |
|
173 |
169 170 171 172
|
syl3anc |
|
174 |
173
|
ralrimiva |
|
175 |
|
brralrspcev |
|
176 |
57 174 175
|
syl2anc |
|
177 |
176
|
adantr |
|
178 |
|
simpr |
|
179 |
|
suprub |
|
180 |
165 167 177 178 179
|
syl31anc |
|
181 |
180 17
|
breqtrrdi |
|
182 |
181
|
ralrimiva |
|
183 |
165 178
|
sseldd |
|
184 |
104
|
adantr |
|
185 |
183 184
|
lenltd |
|
186 |
185
|
ralbidva |
|
187 |
182 186
|
mpbid |
|
188 |
|
ralnex |
|
189 |
187 188
|
sylib |
|
190 |
189
|
adantr |
|
191 |
100 108 190
|
syl2anc |
|
192 |
162 191
|
condan |
|
193 |
|
iccleub |
|
194 |
168 94 98 193
|
syl3anc |
|
195 |
94 99 192 194
|
xrletrid |
|
196 |
16
|
eqcomi |
|
197 |
196
|
a1i |
|
198 |
195 197
|
eleq12d |
|
199 |
93 198
|
mpbird |
|
200 |
|
oveq1 |
|
201 |
200
|
oveq2d |
|
202 |
|
fveq2 |
|
203 |
202
|
fveq1d |
|
204 |
203
|
oveq2d |
|
205 |
204
|
mpteq2dv |
|
206 |
205
|
fveq2d |
|
207 |
206
|
oveq2d |
|
208 |
201 207
|
breq12d |
|
209 |
208
|
elrab |
|
210 |
199 209
|
sylib |
|
211 |
210
|
simprd |
|
212 |
2 3
|
ssfid |
|
213 |
|
eqid |
|
214 |
1 212 5 72 6 7 8 213
|
hoiprodp1 |
|
215 |
|
eqidd |
|
216 |
7
|
adantr |
|
217 |
|
ssun1 |
|
218 |
6
|
eqcomi |
|
219 |
217 218
|
sseqtri |
|
220 |
|
simpr |
|
221 |
219 220
|
sseldi |
|
222 |
216 221
|
ffvelrnd |
|
223 |
8
|
adantr |
|
224 |
223 221
|
ffvelrnd |
|
225 |
221 9
|
syldan |
|
226 |
222 224 225
|
volicon0 |
|
227 |
226
|
prodeq2dv |
|
228 |
14
|
a1i |
|
229 |
219
|
a1i |
|
230 |
7 229
|
fssresd |
|
231 |
8 229
|
fssresd |
|
232 |
1 212 4 230 231
|
hoidmvn0val |
|
233 |
|
fvres |
|
234 |
|
fvres |
|
235 |
233 234
|
oveq12d |
|
236 |
235
|
fveq2d |
|
237 |
236
|
adantl |
|
238 |
|
volico |
|
239 |
222 224 238
|
syl2anc |
|
240 |
239 226
|
eqtr3d |
|
241 |
237 239 240
|
3eqtrd |
|
242 |
241
|
prodeq2dv |
|
243 |
228 232 242
|
3eqtrd |
|
244 |
215 227 243
|
3eqtr4d |
|
245 |
102 57 92
|
volicon0 |
|
246 |
244 245
|
oveq12d |
|
247 |
214 246
|
eqtrd |
|
248 |
247
|
breq1d |
|
249 |
211 248
|
mpbird |
|
250 |
|
0le1 |
|
251 |
250
|
a1i |
|
252 |
15
|
rpge0d |
|
253 |
30 31 251 252
|
addge0d |
|
254 |
81 12 32 253 76
|
lemul2ad |
|
255 |
29 82 83 249 254
|
letrd |
|