Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reconnlem2 Unicode version

Theorem reconnlem2 18811
 Description: Lemma for reconn 18812. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
reconnlem2.1
reconnlem2.2
reconnlem2.3
reconnlem2.4
reconnlem2.5
reconnlem2.6
reconnlem2.7
reconnlem2.8
reconnlem2.9
Assertion
Ref Expression
reconnlem2
Distinct variable groups:   ,,   ,,   ,
Allowed substitution hints:   (,)   ()   (,)   (,)   (,)

Proof of Theorem reconnlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reconnlem2.9 . . . . . . . . . . 11
2 inss2 3522 . . . . . . . . . . . . 13
3 inss2 3522 . . . . . . . . . . . . . . . 16
4 reconnlem2.5 . . . . . . . . . . . . . . . 16
53, 4sseldi 3306 . . . . . . . . . . . . . . 15
6 inss2 3522 . . . . . . . . . . . . . . . 16
7 reconnlem2.6 . . . . . . . . . . . . . . . 16
86, 7sseldi 3306 . . . . . . . . . . . . . . 15
9 reconnlem2.4 . . . . . . . . . . . . . . 15
10 oveq1 6047 . . . . . . . . . . . . . . . . 17
1110sseq1d 3335 . . . . . . . . . . . . . . . 16
12 oveq2 6048 . . . . . . . . . . . . . . . . 17
1312sseq1d 3335 . . . . . . . . . . . . . . . 16
1411, 13rspc2va 3019 . . . . . . . . . . . . . . 15
155, 8, 9, 14syl21anc 1183 . . . . . . . . . . . . . 14
16 reconnlem2.1 . . . . . . . . . . . . . 14
1715, 16sstrd 3318 . . . . . . . . . . . . 13
182, 17syl5ss 3319 . . . . . . . . . . . 12
19 inss1 3521 . . . . . . . . . . . . . . 15
2019, 4sseldi 3306 . . . . . . . . . . . . . 14
2116, 5sseldd 3309 . . . . . . . . . . . . . . . 16
2221rexrd 9090 . . . . . . . . . . . . . . 15
2316, 8sseldd 3309 . . . . . . . . . . . . . . . 16
2423rexrd 9090 . . . . . . . . . . . . . . 15
25 reconnlem2.8 . . . . . . . . . . . . . . 15
26 lbicc2 10969 . . . . . . . . . . . . . . 15
2722, 24, 25, 26syl3anc 1184 . . . . . . . . . . . . . 14
28 elin 3490 . . . . . . . . . . . . . 14
2920, 27, 28sylanbrc 646 . . . . . . . . . . . . 13
30 ne0i 3594 . . . . . . . . . . . . 13
3129, 30syl 16 . . . . . . . . . . . 12
322sseli 3304 . . . . . . . . . . . . . . 15
33 elicc2 10931 . . . . . . . . . . . . . . . . 17
3421, 23, 33syl2anc 643 . . . . . . . . . . . . . . . 16
35 simp3 959 . . . . . . . . . . . . . . . 16
3634, 35syl6bi 220 . . . . . . . . . . . . . . 15
3732, 36syl5 30 . . . . . . . . . . . . . 14
3837ralrimiv 2748 . . . . . . . . . . . . 13
39 breq2 4176 . . . . . . . . . . . . . . 15
4039ralbidv 2686 . . . . . . . . . . . . . 14
4140rspcev 3012 . . . . . . . . . . . . 13
4223, 38, 41syl2anc 643 . . . . . . . . . . . 12
43 suprcl 9924 . . . . . . . . . . . 12
4418, 31, 42, 43syl3anc 1184 . . . . . . . . . . 11
451, 44syl5eqel 2488 . . . . . . . . . 10
46 rphalfcl 10592 . . . . . . . . . 10
47 ltaddrp 10600 . . . . . . . . . 10
4845, 46, 47syl2an 464 . . . . . . . . 9
4945adantr 452 . . . . . . . . . 10
5046rpred 10604 . . . . . . . . . . 11
51 readdcl 9029 . . . . . . . . . . 11
5245, 50, 51syl2an 464 . . . . . . . . . 10
5349, 52ltnled 9176 . . . . . . . . 9
5448, 53mpbid 202 . . . . . . . 8
5518ad2antrr 707 . . . . . . . . . 10
5631ad2antrr 707 . . . . . . . . . 10
5742ad2antrr 707 . . . . . . . . . 10
58 inss1 3521 . . . . . . . . . . . 12
59 simpr 448 . . . . . . . . . . . 12
6058, 59sseldi 3306 . . . . . . . . . . 11
6152adantr 452 . . . . . . . . . . . 12
6221ad2antrr 707 . . . . . . . . . . . . 13
6345ad2antrr 707 . . . . . . . . . . . . 13
64 suprub 9925 . . . . . . . . . . . . . . . 16
6518, 31, 42, 29, 64syl31anc 1187 . . . . . . . . . . . . . . 15
6665, 1syl6breqr 4212 . . . . . . . . . . . . . 14
6766ad2antrr 707 . . . . . . . . . . . . 13
6848adantr 452 . . . . . . . . . . . . . 14
6963, 61, 68ltled 9177 . . . . . . . . . . . . 13
7062, 63, 61, 67, 69letrd 9183 . . . . . . . . . . . 12
7123ad2antrr 707 . . . . . . . . . . . . 13
72 inss2 3522 . . . . . . . . . . . . . . 15
7372, 59sseldi 3306 . . . . . . . . . . . . . 14
74 eliooord 10926 . . . . . . . . . . . . . . 15
7574simprd 450 . . . . . . . . . . . . . 14
7673, 75syl 16 . . . . . . . . . . . . 13
7761, 71, 76ltled 9177 . . . . . . . . . . . 12
78 elicc2 10931 . . . . . . . . . . . . 13
7962, 71, 78syl2anc 643 . . . . . . . . . . . 12
8061, 70, 77, 79mpbir3and 1137 . . . . . . . . . . 11
81 elin 3490 . . . . . . . . . . 11
8260, 80, 81sylanbrc 646 . . . . . . . . . 10
83 suprub 9925 . . . . . . . . . 10
8455, 56, 57, 82, 83syl31anc 1187 . . . . . . . . 9
8584, 1syl6breqr 4212 . . . . . . . 8
8654, 85mtand 641 . . . . . . 7
87 eqid 2404 . . . . . . . . . . . . 13
8887remetdval 18773 . . . . . . . . . . . 12
8952, 49, 88syl2anc 643 . . . . . . . . . . 11
9049recnd 9070 . . . . . . . . . . . . 13
9150adantl 453 . . . . . . . . . . . . . 14
9291recnd 9070 . . . . . . . . . . . . 13
9390, 92pncan2d 9369 . . . . . . . . . . . 12
9493fveq2d 5691 . . . . . . . . . . 11
9546adantl 453 . . . . . . . . . . . 12
96 rpre 10574 . . . . . . . . . . . . 13
97 rpge0 10580 . . . . . . . . . . . . 13
9896, 97absidd 12180 . . . . . . . . . . . 12
9995, 98syl 16 . . . . . . . . . . 11
10089, 94, 993eqtrd 2440 . . . . . . . . . 10
101 rphalflt 10594 . . . . . . . . . . 11
102101adantl 453 . . . . . . . . . 10
103100, 102eqbrtrd 4192 . . . . . . . . 9
10487rexmet 18775 . . . . . . . . . . 11
105104a1i 11 . . . . . . . . . 10
106 rpxr 10575 . . . . . . . . . . 11
107106adantl 453 . . . . . . . . . 10
108 elbl3 18375 . . . . . . . . . 10
109105, 107, 49, 52, 108syl22anc 1185 . . . . . . . . 9
110103, 109mpbird 224 . . . . . . . 8
111 ssel 3302 . . . . . . . 8
112110, 111syl5com 28 . . . . . . 7
11386, 112mtod 170 . . . . . 6
114113nrexdv 2769 . . . . 5
11545adantr 452 . . . . . . . . 9
116 mnflt 10678 . . . . . . . . . 10
117115, 116syl 16 . . . . . . . . 9
118 suprleub 9928 . . . . . . . . . . . . . . . . 17
11918, 31, 42, 23, 118syl31anc 1187 . . . . . . . . . . . . . . . 16
12038, 119mpbird 224 . . . . . . . . . . . . . . 15
1211, 120syl5eqbr 4205 . . . . . . . . . . . . . 14
12245, 23leloed 9172 . . . . . . . . . . . . . 14
123121, 122mpbid 202 . . . . . . . . . . . . 13
124123ord 367 . . . . . . . . . . . 12
125 elndif 3431 . . . . . . . . . . . . . . 15
1268, 125syl 16 . . . . . . . . . . . . . 14
127 inss1 3521 . . . . . . . . . . . . . . . 16
128127, 7sseldi 3306 . . . . . . . . . . . . . . 15
129 elin 3490 . . . . . . . . . . . . . . . 16
130 reconnlem2.7 . . . . . . . . . . . . . . . . 17
131130sseld 3307 . . . . . . . . . . . . . . . 16
132129, 131syl5bir 210 . . . . . . . . . . . . . . 15
133128, 132mpan2d 656 . . . . . . . . . . . . . 14
134126, 133mtod 170 . . . . . . . . . . . . 13
135 eleq1 2464 . . . . . . . . . . . . . 14
136135notbid 286 . . . . . . . . . . . . 13
137134, 136syl5ibrcom 214 . . . . . . . . . . . 12
138124, 137syld 42 . . . . . . . . . . 11
139138con4d 99 . . . . . . . . . 10
140139imp 419 . . . . . . . . 9
141 mnfxr 10670 . . . . . . . . . . 11
142 elioo2 10913 . . . . . . . . . . 11
143141, 24, 142sylancr 645 . . . . . . . . . 10
144143adantr 452 . . . . . . . . 9
145115, 117, 140, 144mpbir3and 1137 . . . . . . . 8
146145ex 424 . . . . . . 7
147146ancld 537 . . . . . 6
148 elin 3490 . . . . . . 7
149 reconnlem2.2 . . . . . . . 8
150 retop 18748 . . . . . . . . 9
151 iooretop 18753 . . . . . . . . 9
152 inopn 16927 . . . . . . . . 9
153150, 151, 152mp3an13 1270 . . . . . . . 8
154 eqid 2404 . . . . . . . . . . . 12
15587, 154tgioo 18780 . . . . . . . . . . 11
156155mopni2 18476 . . . . . . . . . 10
157104, 156mp3an1 1266 . . . . . . . . 9
158157ex 424 . . . . . . . 8
159149, 153, 1583syl 19 . . . . . . 7
160148, 159syl5bir 210 . . . . . 6
161147, 160syld 42 . . . . 5
162114, 161mtod 170 . . . 4
163 ltsubrp 10599 . . . . . . . . 9
16445, 163sylan 458 . . . . . . . 8
165 rpre 10574 . . . . . . . . . 10
166 resubcl 9321 . . . . . . . . . 10
16745, 165, 166syl2an 464 . . . . . . . . 9
168167, 49ltnled 9176 . . . . . . . 8
169164, 168mpbid 202 . . . . . . 7
17087bl2ioo 18776 . . . . . . . . . 10
17145, 165, 170syl2an 464 . . . . . . . . 9
172171sseq1d 3335 . . . . . . . 8
17315ad2antrr 707 . . . . . . . . . . . . . . . . 17
1742, 173syl5ss 3319 . . . . . . . . . . . . . . . 16
175174sselda 3308 . . . . . . . . . . . . . . 15
176 elndif 3431 . . . . . . . . . . . . . . 15
177175, 176syl 16 . . . . . . . . . . . . . 14
178130ad3antrrr 711 . . . . . . . . . . . . . . . 16
179 inss1 3521 . . . . . . . . . . . . . . . . . 18
180 simprl 733 . . . . . . . . . . . . . . . . . 18
181179, 180sseldi 3306 . . . . . . . . . . . . . . . . 17
182 simplr 732 . . . . . . . . . . . . . . . . . 18
18318ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . 21
184 simpr 448 . . . . . . . . . . . . . . . . . . . . 21
185183, 184sseldd 3309 . . . . . . . . . . . . . . . . . . . 20
186185adantrr 698 . . . . . . . . . . . . . . . . . . 19
187 simprr 734 . . . . . . . . . . . . . . . . . . 19
18849ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
189 simpllr 736 . . . . . . . . . . . . . . . . . . . . . 22
190189rpred 10604 . . . . . . . . . . . . . . . . . . . . 21
191188, 190readdcld 9071 . . . . . . . . . . . . . . . . . . . 20
192183adantrr 698 . . . . . . . . . . . . . . . . . . . . . 22
19331ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 22
19442ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 22
195 suprub 9925 . . . . . . . . . . . . . . . . . . . . . 22
196192, 193, 194, 180, 195syl31anc 1187 . . . . . . . . . . . . . . . . . . . . 21
197196, 1syl6breqr 4212 . . . . . . . . . . . . . . . . . . . 20
198188, 189ltaddrpd 10633 . . . . . . . . . . . . . . . . . . . 20
199186, 188, 191, 197, 198lelttrd 9184 . . . . . . . . . . . . . . . . . . 19
200167ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
201 rexr 9086 . . . . . . . . . . . . . . . . . . . . 21
202 rexr 9086 . . . . . . . . . . . . . . . . . . . . 21
203 elioo2 10913 . . . . . . . . . . . . . . . . . . . . 21
204201, 202, 203syl2an 464 . . . . . . . . . . . . . . . . . . . 20
205200, 191, 204syl2anc 643 . . . . . . . . . . . . . . . . . . 19
206186, 187, 199, 205mpbir3and 1137 . . . . . . . . . . . . . . . . . 18
207182, 206sseldd 3309 . . . . . . . . . . . . . . . . 17
208 elin 3490 . . . . . . . . . . . . . . . . 17
209181, 207, 208sylanbrc 646 . . . . . . . . . . . . . . . 16
210178, 209sseldd 3309 . . . . . . . . . . . . . . 15
211210expr 599 . . . . . . . . . . . . . 14
212177, 211mtod 170 . . . . . . . . . . . . 13
213167ad2antrr 707 . . . . . . . . . . . . . 14
214185, 213lenltd 9175 . . . . . . . . . . . . 13
215212, 214mpbird 224 . . . . . . . . . . . 12
216215ralrimiva 2749 . . . . . . . . . . 11
21718ad2antrr 707 . . . . . . . . . . . 12
21831ad2antrr 707 . . . . . . . . . . . 12
21942ad2antrr 707 . . . . . . . . . . . 12
220167adantr 452 . . . . . . . . . . . 12
221 suprleub 9928 . . . . . . . . . . . 12
222217, 218, 219, 220, 221syl31anc 1187 . . . . . . . . . . 11
223216, 222mpbird 224 . . . . . . . . . 10
2241, 223syl5eqbr 4205 . . . . . . . . 9
225224ex 424 . . . . . . . 8
226172, 225sylbid 207 . . . . . . 7
227169, 226mtod 170 . . . . . 6
228227nrexdv 2769 . . . . 5
229 reconnlem2.3 . . . . . 6
230155mopni2 18476 . . . . . . . 8
231104, 230mp3an1 1266 . . . . . . 7
232231ex 424 . . . . . 6
233229, 232syl 16 . . . . 5
234228, 233mtod 170 . . . 4
235 ioran 477 . . . 4
236162, 234, 235sylanbrc 646 . . 3
237 elun 3448 . . 3
238236, 237sylnibr 297 . 2
239 elicc2 10931 . . . . . 6
24021, 23, 239syl2anc 643 . . . . 5
24145, 66, 121, 240mpbir3and 1137 . . . 4
24215, 241sseldd 3309 . . 3
243 ssel 3302 . . 3
244242, 243syl5com 28 . 2
245238, 244mtod 170 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667   cdif 3277   cun 3278   cin 3279   wss 3280  c0 3588   class class class wbr 4172   cxp 4835   crn 4838   cres 4839   ccom 4841  cfv 5413  (class class class)co 6040  csup 7403  cr 8945   caddc 8949   cmnf 9074  cxr 9075   clt 9076   cle 9077   cmin 9247   cdiv 9633  c2 10005  crp 10568  cioo 10872  cicc 10875  cabs 11994  ctg 13620  cxmt 16641  cbl 16643  cmopn 16646  ctop 16913 This theorem is referenced by:  reconn  18812 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-icc 10879  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-topgen 13622  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-top 16918  df-bases 16920  df-topon 16921
 Copyright terms: Public domain W3C validator