Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem3 Structured version   Unicode version

Theorem heiborlem3 26513
 Description: Lemma for heibor 26521. Using countable choice ax-cc 8307, we have fixed in advance a collection of finite nets for (note that an -net is a set of points in whose -balls cover ). The set is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set ). If the theorem was false, then would be in , and so some ball at each level would also be in . But we can say more than this; given a ball on level , since level covers the space and thus also , using heiborlem1 26511 there is a ball on the next level whose intersection with also has no finite subcover. Now since the set is a countable union of finite sets, it is countable (which needs ax-cc 8307 via iunctb 8441), and so we can apply ax-cc 8307 to directly to get a function from to itself, which points from each ball in to a ball on the next level in , and such that the intersection between these balls is also in . (Contributed by Jeff Madsen, 18-Jan-2014.)
Hypotheses
Ref Expression
heibor.1
heibor.3
heibor.4
heibor.5
heibor.6
heibor.7
heibor.8
Assertion
Ref Expression
heiborlem3
Distinct variable groups:   ,,,,   ,,   ,,   ,,,,,,,,   ,,,,,   ,,,,,,,,   ,,,,,,,   ,,,,,,,,   ,,,,,   ,
Allowed substitution hints:   (,,,,,)   (,)   ()   (,,,)   (,,,,,)   (,,)

Proof of Theorem heiborlem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nn0ex 10219 . . . . . 6
2 fvex 5734 . . . . . . 7
3 snex 4397 . . . . . . 7
42, 3xpex 4982 . . . . . 6
51, 4iunex 5983 . . . . 5
6 heibor.4 . . . . . . . . 9
76relopabi 4992 . . . . . . . 8
8 1st2nd 6385 . . . . . . . 8
97, 8mpan 652 . . . . . . 7
109eleq1d 2501 . . . . . . . . . . 11
11 df-br 4205 . . . . . . . . . . 11
1210, 11syl6bbr 255 . . . . . . . . . 10
13 heibor.1 . . . . . . . . . . 11
14 heibor.3 . . . . . . . . . . 11
15 fvex 5734 . . . . . . . . . . 11
16 fvex 5734 . . . . . . . . . . 11
1713, 14, 6, 15, 16heiborlem2 26512 . . . . . . . . . 10
1812, 17syl6bb 253 . . . . . . . . 9
1918ibi 233 . . . . . . . 8
2016snid 3833 . . . . . . . . . . . 12
21 opelxp 4900 . . . . . . . . . . . 12
2220, 21mpbiran2 886 . . . . . . . . . . 11
23 fveq2 5720 . . . . . . . . . . . . . 14
24 sneq 3817 . . . . . . . . . . . . . 14
2523, 24xpeq12d 4895 . . . . . . . . . . . . 13
2625eleq2d 2502 . . . . . . . . . . . 12
2726rspcev 3044 . . . . . . . . . . 11
2822, 27sylan2br 463 . . . . . . . . . 10
29 eliun 4089 . . . . . . . . . 10
3028, 29sylibr 204 . . . . . . . . 9
31303adant3 977 . . . . . . . 8
3219, 31syl 16 . . . . . . 7
339, 32eqeltrd 2509 . . . . . 6
3433ssriv 3344 . . . . 5
35 ssdomg 7145 . . . . 5
365, 34, 35mp2 9 . . . 4
37 nn0ennn 11310 . . . . . . 7
38 nnenom 11311 . . . . . . 7
3937, 38entri 7153 . . . . . 6
40 endom 7126 . . . . . 6
4139, 40ax-mp 8 . . . . 5
42 vex 2951 . . . . . . . 8
432, 42xpsnen 7184 . . . . . . 7
44 inss2 3554 . . . . . . . . 9
45 heibor.7 . . . . . . . . . 10
4645ffvelrnda 5862 . . . . . . . . 9
4744, 46sseldi 3338 . . . . . . . 8
48 isfinite 7599 . . . . . . . . 9
49 sdomdom 7127 . . . . . . . . 9
5048, 49sylbi 188 . . . . . . . 8
5147, 50syl 16 . . . . . . 7
52 endomtr 7157 . . . . . . 7
5343, 51, 52sylancr 645 . . . . . 6
5453ralrimiva 2781 . . . . 5
55 iunctb 8441 . . . . 5
5641, 54, 55sylancr 645 . . . 4
57 domtr 7152 . . . 4
5836, 56, 57sylancr 645 . . 3
5919simp1d 969 . . . . . . . . 9
60 peano2nn0 10252 . . . . . . . . 9
6159, 60syl 16 . . . . . . . 8
62 ffvelrn 5860 . . . . . . . 8
6345, 61, 62syl2an 464 . . . . . . 7
6444, 63sseldi 3338 . . . . . 6
65 iunin2 4147 . . . . . . . 8
66 heibor.8 . . . . . . . . . . 11
67 oveq1 6080 . . . . . . . . . . . . . . . 16
6867cbviunv 4122 . . . . . . . . . . . . . . 15
69 fveq2 5720 . . . . . . . . . . . . . . . 16
7069iuneq1d 4108 . . . . . . . . . . . . . . 15
7168, 70syl5eq 2479 . . . . . . . . . . . . . 14
72 oveq2 6081 . . . . . . . . . . . . . . 15
7372iuneq2d 4110 . . . . . . . . . . . . . 14
7471, 73eqtrd 2467 . . . . . . . . . . . . 13
7574eqeq2d 2446 . . . . . . . . . . . 12
7675rspccva 3043 . . . . . . . . . . 11
7766, 61, 76syl2an 464 . . . . . . . . . 10
7877ineq2d 3534 . . . . . . . . 9
799fveq2d 5724 . . . . . . . . . . . . . 14
80 df-ov 6076 . . . . . . . . . . . . . 14
8179, 80syl6eqr 2485 . . . . . . . . . . . . 13
8281adantl 453 . . . . . . . . . . . 12
83 inss1 3553 . . . . . . . . . . . . . . . 16
84 ffvelrn 5860 . . . . . . . . . . . . . . . . 17
8545, 59, 84syl2an 464 . . . . . . . . . . . . . . . 16
8683, 85sseldi 3338 . . . . . . . . . . . . . . 15
8786elpwid 3800 . . . . . . . . . . . . . 14
8819simp2d 970 . . . . . . . . . . . . . . 15
8988adantl 453 . . . . . . . . . . . . . 14
9087, 89sseldd 3341 . . . . . . . . . . . . 13
9159adantl 453 . . . . . . . . . . . . 13
92 oveq1 6080 . . . . . . . . . . . . . 14
93 oveq2 6081 . . . . . . . . . . . . . . . 16
9493oveq2d 6089 . . . . . . . . . . . . . . 15
9594oveq2d 6089 . . . . . . . . . . . . . 14
96 heibor.5 . . . . . . . . . . . . . 14
97 ovex 6098 . . . . . . . . . . . . . 14
9892, 95, 96, 97ovmpt2 6201 . . . . . . . . . . . . 13
9990, 91, 98syl2anc 643 . . . . . . . . . . . 12
10082, 99eqtrd 2467 . . . . . . . . . . 11
101 heibor.6 . . . . . . . . . . . . . . 15
102 cmetmet 19231 . . . . . . . . . . . . . . 15
103101, 102syl 16 . . . . . . . . . . . . . 14
104 metxmet 18356 . . . . . . . . . . . . . 14
105103, 104syl 16 . . . . . . . . . . . . 13
106105adantr 452 . . . . . . . . . . . 12
107 2nn 10125 . . . . . . . . . . . . . . . 16
108 nnexpcl 11386 . . . . . . . . . . . . . . . 16
109107, 91, 108sylancr 645 . . . . . . . . . . . . . . 15
110109nnrpd 10639 . . . . . . . . . . . . . 14
111110rpreccld 10650 . . . . . . . . . . . . 13
112111rpxrd 10641 . . . . . . . . . . . 12
113 blssm 18440 . . . . . . . . . . . 12
114106, 90, 112, 113syl3anc 1184 . . . . . . . . . . 11
115100, 114eqsstrd 3374 . . . . . . . . . 10
116 df-ss 3326 . . . . . . . . . 10
117115, 116sylib 189 . . . . . . . . 9
11878, 117eqtr3d 2469 . . . . . . . 8
11965, 118syl5eq 2479 . . . . . . 7
120 eqimss2 3393 . . . . . . 7
121119, 120syl 16 . . . . . 6
12219simp3d 971 . . . . . . . 8
12381, 122eqeltrd 2509 . . . . . . 7
124123adantl 453 . . . . . 6
125 fvex 5734 . . . . . . . 8
126125inex1 4336 . . . . . . 7
12713, 14, 126heiborlem1 26511 . . . . . 6
12864, 121, 124, 127syl3anc 1184 . . . . 5
12983, 63sseldi 3338 . . . . . . . . . . . 12
130129elpwid 3800 . . . . . . . . . . 11
13113mopnuni 18463 . . . . . . . . . . . . 13
132105, 131syl 16 . . . . . . . . . . . 12
133132adantr 452 . . . . . . . . . . 11
134130, 133sseqtrd 3376 . . . . . . . . . 10
135134sselda 3340 . . . . . . . . 9
136135adantrr 698 . . . . . . . 8
13761adantl 453 . . . . . . . . . 10
138 id 20 . . . . . . . . . 10
139 snfi 7179 . . . . . . . . . . . 12
140 inss2 3554 . . . . . . . . . . . . 13
141 ovex 6098 . . . . . . . . . . . . . . 15
142141unisn 4023 . . . . . . . . . . . . . 14
143 uniiun 4136 . . . . . . . . . . . . . 14
144142, 143eqtr3i 2457 . . . . . . . . . . . . 13
145140, 144sseqtri 3372 . . . . . . . . . . . 12
146 vex 2951 . . . . . . . . . . . . 13
14713, 14, 146heiborlem1 26511 . . . . . . . . . . . 12
148139, 145, 147mp3an12 1269 . . . . . . . . . . 11
149 eleq1 2495 . . . . . . . . . . . 12
150141, 149rexsn 3842 . . . . . . . . . . 11
151148, 150sylib 189 . . . . . . . . . 10
152 ovex 6098 . . . . . . . . . . . 12
15313, 14, 6, 42, 152heiborlem2 26512 . . . . . . . . . . 11
154153biimpri 198 . . . . . . . . . 10
155137, 138, 151, 154syl3an 1226 . . . . . . . . 9
1561553expb 1154 . . . . . . . 8
157 simprr 734 . . . . . . . 8
158136, 156, 157jca32 522 . . . . . . 7
159158ex 424 . . . . . 6
160159reximdv2 2807 . . . . 5
161128, 160mpd 15 . . . 4
162161ralrimiva 2781 . . 3
163 fvex 5734 . . . . . 6
16413, 163eqeltri 2505 . . . . 5
165164uniex 4697 . . . 4
166 breq1 4207 . . . . 5
167 oveq1 6080 . . . . . . 7
168167ineq2d 3534 . . . . . 6
169168eleq1d 2501 . . . . 5
170166, 169anbi12d 692 . . . 4
171165, 170axcc4dom 8313 . . 3
17258, 162, 171syl2anc 643 . 2
173 simpr 448 . . 3
174173eximi 1585 . 2
175172, 174syl 16 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725  cab 2421  wral 2697  wrex 2698  cvv 2948   cin 3311   wss 3312  cpw 3791  csn 3806  cop 3809  cuni 4007  ciun 4085   class class class wbr 4204  copab 4257  com 4837   cxp 4868   wrel 4875  wf 5442  cfv 5446  (class class class)co 6073   cmpt2 6075  c1st 6339  c2nd 6340   cen 7098   cdom 7099   csdm 7100  cfn 7101  c1 8983   caddc 8985  cxr 9111   cdiv 9669  cn 9992  c2 10041  cn0 10213  cexp 11374  cxmt 16678  cme 16679  cbl 16680  cmopn 16683  cms 19199 This theorem is referenced by:  heiborlem10  26520 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7588  ax-cc 8307  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059  ax-pre-sup 9060 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-oadd 6720  df-er 6897  df-map 7012  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-sup 7438  df-oi 7471  df-card 7818  df-acn 7821  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-div 9670  df-nn 9993  df-2 10050  df-n0 10214  df-z 10275  df-uz 10481  df-q 10567  df-rp 10605  df-xneg 10702  df-xadd 10703  df-xmul 10704  df-seq 11316  df-exp 11375  df-topgen 13659  df-psmet 16686  df-xmet 16687  df-met 16688  df-bl 16689  df-mopn 16690  df-top 16955  df-bases 16957  df-topon 16958  df-cmet 19202
 Copyright terms: Public domain W3C validator