Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  locfinreflem Structured version   Visualization version   Unicode version

Theorem locfinreflem 28741
 Description: A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function from the original cover , which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.)
Hypotheses
Ref Expression
locfinref.x
locfinref.1
locfinref.2
locfinref.3
locfinref.4
locfinref.5
Assertion
Ref Expression
locfinreflem
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem locfinreflem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 locfinref.4 . . . 4
2 locfinref.5 . . . . 5
3 reff 28740 . . . . 5
42, 3syl 17 . . . 4
51, 4mpbid 215 . . 3
65simprd 470 . 2
7 funmpt 5625 . . . . . 6
87a1i 11 . . . . 5
9 eqid 2471 . . . . . . 7
109dmmptss 5338 . . . . . 6
11 frn 5747 . . . . . . 7
1211ad2antlr 741 . . . . . 6
1310, 12syl5ss 3429 . . . . 5
14 locfintop 20613 . . . . . . . . . 10
152, 14syl 17 . . . . . . . . 9
1615ad3antrrr 744 . . . . . . . 8
17 cnvimass 5194 . . . . . . . . . 10
18 fdm 5745 . . . . . . . . . . 11
1918ad3antlr 745 . . . . . . . . . 10
2017, 19syl5sseq 3466 . . . . . . . . 9
21 locfinref.3 . . . . . . . . . 10
2221ad3antrrr 744 . . . . . . . . 9
2320, 22sstrd 3428 . . . . . . . 8
24 uniopn 20004 . . . . . . . 8
2516, 23, 24syl2anc 673 . . . . . . 7
2625ralrimiva 2809 . . . . . 6
279rnmptss 6068 . . . . . 6
2826, 27syl 17 . . . . 5
29 eqid 2471 . . . . . . . . . 10
30 eqid 2471 . . . . . . . . . 10
3129, 30refbas 20602 . . . . . . . . 9
321, 31syl 17 . . . . . . . 8
3332ad2antrr 740 . . . . . . 7
34 nfv 1769 . . . . . . . . . . . . 13
35 nfra1 2785 . . . . . . . . . . . . 13
3634, 35nfan 2031 . . . . . . . . . . . 12
37 nfre1 2846 . . . . . . . . . . . 12
3836, 37nfan 2031 . . . . . . . . . . 11
39 ffn 5739 . . . . . . . . . . . . . . 15
4039ad4antlr 747 . . . . . . . . . . . . . 14
41 simplr 770 . . . . . . . . . . . . . 14
42 fnfvelrn 6034 . . . . . . . . . . . . . 14
4340, 41, 42syl2anc 673 . . . . . . . . . . . . 13
44 ssid 3437 . . . . . . . . . . . . . . 15
4539ad3antlr 745 . . . . . . . . . . . . . . . 16
46 eqid 2471 . . . . . . . . . . . . . . . . 17
47 fniniseg 6018 . . . . . . . . . . . . . . . . . 18
4847biimpar 493 . . . . . . . . . . . . . . . . 17
4946, 48mpanr2 698 . . . . . . . . . . . . . . . 16
5045, 49sylancom 680 . . . . . . . . . . . . . . 15
51 ssuni 4212 . . . . . . . . . . . . . . 15
5244, 50, 51sylancr 676 . . . . . . . . . . . . . 14
5352sselda 3418 . . . . . . . . . . . . 13
54 sneq 3969 . . . . . . . . . . . . . . . . 17
5554imaeq2d 5174 . . . . . . . . . . . . . . . 16
5655unieqd 4200 . . . . . . . . . . . . . . 15
5756eleq2d 2534 . . . . . . . . . . . . . 14
5857rspcev 3136 . . . . . . . . . . . . 13
5943, 53, 58syl2anc 673 . . . . . . . . . . . 12
6059adantllr 733 . . . . . . . . . . 11
61 simpr 468 . . . . . . . . . . 11
6238, 60, 61r19.29af 2916 . . . . . . . . . 10
63 nfv 1769 . . . . . . . . . . . . . 14
6436, 63nfan 2031 . . . . . . . . . . . . 13
65 nfv 1769 . . . . . . . . . . . . 13
6664, 65nfan 2031 . . . . . . . . . . . 12
6720ad3antrrr 744 . . . . . . . . . . . . 13
68 simplr 770 . . . . . . . . . . . . 13
6967, 68sseldd 3419 . . . . . . . . . . . 12
70 simpr 468 . . . . . . . . . . . 12
71 simpr 468 . . . . . . . . . . . . 13
72 eluni2 4194 . . . . . . . . . . . . 13
7371, 72sylib 201 . . . . . . . . . . . 12
7466, 69, 70, 73reximd2a 2854 . . . . . . . . . . 11
7574r19.29an 2917 . . . . . . . . . 10
7662, 75impbida 850 . . . . . . . . 9
77 eluni2 4194 . . . . . . . . 9
78 eliun 4274 . . . . . . . . 9
7976, 77, 783bitr4g 296 . . . . . . . 8
8079eqrdv 2469 . . . . . . 7
81 dfiun3g 5093 . . . . . . . 8
8226, 81syl 17 . . . . . . 7
8333, 80, 823eqtrd 2509 . . . . . 6
8411ad3antlr 745 . . . . . . . . 9
85 vex 3034 . . . . . . . . . . 11
869elrnmpt 5087 . . . . . . . . . . 11
8785, 86mp1i 13 . . . . . . . . . 10
8887biimpa 492 . . . . . . . . 9
89 ssrexv 3480 . . . . . . . . 9
9084, 88, 89sylc 61 . . . . . . . 8
91 nfv 1769 . . . . . . . . . 10
92 nfmpt1 4485 . . . . . . . . . . . 12
9392nfrn 5083 . . . . . . . . . . 11
9493nfcri 2606 . . . . . . . . . 10
9591, 94nfan 2031 . . . . . . . . 9
96 simpr 468 . . . . . . . . . . 11
97 nfv 1769 . . . . . . . . . . . . . . . 16
9836, 97nfan 2031 . . . . . . . . . . . . . . 15
99 nfv 1769 . . . . . . . . . . . . . . 15
10098, 99nfan 2031 . . . . . . . . . . . . . 14
101 nfv 1769 . . . . . . . . . . . . . 14
102100, 101nfan 2031 . . . . . . . . . . . . 13
103 simp-5r 787 . . . . . . . . . . . . . . . 16
10439ad5antlr 749 . . . . . . . . . . . . . . . . . . 19
105 fniniseg 6018 . . . . . . . . . . . . . . . . . . 19
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18
107106biimpa 492 . . . . . . . . . . . . . . . . 17
108107simpld 466 . . . . . . . . . . . . . . . 16
109 rspa 2774 . . . . . . . . . . . . . . . 16
110103, 108, 109syl2anc 673 . . . . . . . . . . . . . . 15
111107simprd 470 . . . . . . . . . . . . . . 15
112110, 111sseqtrd 3454 . . . . . . . . . . . . . 14
113112ex 441 . . . . . . . . . . . . 13
114102, 113ralrimi 2800 . . . . . . . . . . . 12
115 unissb 4221 . . . . . . . . . . . 12
116114, 115sylibr 217 . . . . . . . . . . 11
11796, 116eqsstrd 3452 . . . . . . . . . 10
118117exp31 615 . . . . . . . . 9
11995, 118reximdai 2853 . . . . . . . 8
12090, 119mpd 15 . . . . . . 7
121120ralrimiva 2809 . . . . . 6
122 vex 3034 . . . . . . . . . 10
123122rnex 6746 . . . . . . . . 9
124123mptex 6152 . . . . . . . 8
125 rnexg 6744 . . . . . . . 8
126124, 125mp1i 13 . . . . . . 7
127 eqid 2471 . . . . . . . 8
128127, 30isref 20601 . . . . . . 7
129126, 128syl 17 . . . . . 6
13083, 121, 129mpbir2and 936 . . . . 5
13115ad2antrr 740 . . . . . 6
132 locfinref.2 . . . . . . . 8
133132ad2antrr 740 . . . . . . 7
134133, 83eqtrd 2505 . . . . . 6
135 nfv 1769 . . . . . . . . 9
13636, 135nfan 2031 . . . . . . . 8
137 simplr 770 . . . . . . . 8
138 ffun 5742 . . . . . . . . . . . . . 14
139138ad6antlr 751 . . . . . . . . . . . . 13
140 imafi 7885 . . . . . . . . . . . . 13
141139, 140sylancom 680 . . . . . . . . . . . 12
142 simp3 1032 . . . . . . . . . . . . . . . . . . 19
143 sneq 3969 . . . . . . . . . . . . . . . . . . . . . . 23
144143imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . . 22
145144unieqd 4200 . . . . . . . . . . . . . . . . . . . . 21
146122cnvex 6759 . . . . . . . . . . . . . . . . . . . . . . 23
147 imaexg 6749 . . . . . . . . . . . . . . . . . . . . . . 23
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22
149148uniex 6606 . . . . . . . . . . . . . . . . . . . . 21
150145, 9, 149fvmpt 5963 . . . . . . . . . . . . . . . . . . . 20
1511503ad2ant2 1052 . . . . . . . . . . . . . . . . . . 19
152142, 151eqtrd 2505 . . . . . . . . . . . . . . . . . 18
153152ineq1d 3624 . . . . . . . . . . . . . . . . 17
154153neeq1d 2702 . . . . . . . . . . . . . . . 16
155123a1i 11 . . . . . . . . . . . . . . . 16
156 imaexg 6749 . . . . . . . . . . . . . . . . . . . . 21
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
158157uniex 6606 . . . . . . . . . . . . . . . . . . 19
159158, 9fnmpti 5716 . . . . . . . . . . . . . . . . . 18
160 dffn4 5812 . . . . . . . . . . . . . . . . . 18
161159, 160mpbi 213 . . . . . . . . . . . . . . . . 17
162161a1i 11 . . . . . . . . . . . . . . . 16
163154, 155, 162rabfodom 28219 . . . . . . . . . . . . . . 15
164 sneq 3969 . . . . . . . . . . . . . . . . . . . 20
165164imaeq2d 5174 . . . . . . . . . . . . . . . . . . 19
166165unieqd 4200 . . . . . . . . . . . . . . . . . 18
167166ineq1d 3624 . . . . . . . . . . . . . . . . 17
168167neeq1d 2702 . . . . . . . . . . . . . . . 16
169168cbvrabv 3030 . . . . . . . . . . . . . . 15
170163, 169syl6breq 4435 . . . . . . . . . . . . . 14
171123rabex 4550 . . . . . . . . . . . . . . 15
172 nfv 1769 . . . . . . . . . . . . . . . . . . . . 21
173 nfrab1 2957 . . . . . . . . . . . . . . . . . . . . . 22
174173nfel1 2626 . . . . . . . . . . . . . . . . . . . . 21
175172, 174nfan 2031 . . . . . . . . . . . . . . . . . . . 20
176 nfv 1769 . . . . . . . . . . . . . . . . . . . 20
177175, 176nfan 2031 . . . . . . . . . . . . . . . . . . 19
178 nfv 1769 . . . . . . . . . . . . . . . . . . 19
179177, 178nfan 2031 . . . . . . . . . . . . . . . . . 18
180 nfv 1769 . . . . . . . . . . . . . . . . . . 19
181173, 180nfrex 2848 . . . . . . . . . . . . . . . . . 18
18239ad5antlr 749 . . . . . . . . . . . . . . . . . . . . . . 23
183182ad5antr 748 . . . . . . . . . . . . . . . . . . . . . 22
184 simplr 770 . . . . . . . . . . . . . . . . . . . . . 22
185 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . . . 23
186185biimpa 492 . . . . . . . . . . . . . . . . . . . . . 22
187183, 184, 186syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
188187simpld 466 . . . . . . . . . . . . . . . . . . . 20
189 simpr 468 . . . . . . . . . . . . . . . . . . . 20
190 rabid 2953 . . . . . . . . . . . . . . . . . . . 20
191188, 189, 190sylanbrc 677 . . . . . . . . . . . . . . . . . . 19
192187simprd 470 . . . . . . . . . . . . . . . . . . 19
193 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
194193eqeq1d 2473 . . . . . . . . . . . . . . . . . . . 20
195194rspcev 3136 . . . . . . . . . . . . . . . . . . 19
196191, 192, 195syl2anc 673 . . . . . . . . . . . . . . . . . 18
197 uniinn0 28241 . . . . . . . . . . . . . . . . . . . 20
198197biimpi 199 . . . . . . . . . . . . . . . . . . 19
199198adantl 473 . . . . . . . . . . . . . . . . . 18
200179, 181, 196, 199r19.29af2 2915 . . . . . . . . . . . . . . . . 17
201200ex 441 . . . . . . . . . . . . . . . 16
202201ss2rabdv 3496 . . . . . . . . . . . . . . 15
203 ssdomg 7633 . . . . . . . . . . . . . . 15
204171, 202, 203mpsyl 64 . . . . . . . . . . . . . 14
205 domtr 7640 . . . . . . . . . . . . . 14
206170, 204, 205syl2anc 673 . . . . . . . . . . . . 13
207182adantr 472 . . . . . . . . . . . . . 14
208 dffn3 5748 . . . . . . . . . . . . . . 15
209208biimpi 199 . . . . . . . . . . . . . 14
210 ssrab2 3500 . . . . . . . . . . . . . . 15
211 fimarab 28320 . . . . . . . . . . . . . . 15
212210, 211mpan2 685 . . . . . . . . . . . . . 14
213207, 209, 2123syl 18 . . . . . . . . . . . . 13
214206, 213breqtrrd 4422 . . . . . . . . . . . 12
215 domfi 7811 . . . . . . . . . . . 12
216141, 214, 215syl2anc 673 . . . . . . . . . . 11
217216ex 441 . . . . . . . . . 10
218217imdistanda 707 . . . . . . . . 9
219218imp 436 . . . . . . . 8
220 simplll 776 . . . . . . . . 9
221 locfinref.x . . . . . . . . . . . . 13
222221, 29islocfin 20609 . . . . . . . . . . . 12
2232, 222sylib 201 . . . . . . . . . . 11
224223simp3d 1044 . . . . . . . . . 10
225224r19.21bi 2776 . . . . . . . . 9
226220, 225sylancom 680 . . . . . . . 8
227136, 137, 219, 226reximd2a 2854 . . . . . . 7
228227ralrimiva 2809 . . . . . 6
229221, 127islocfin 20609 . . . . . 6
230131, 134, 228, 229syl3anbrc 1214 . . . . 5
231 funeq 5608 . . . . . . . 8
232 dmeq 5040 . . . . . . . . 9
233232sseq1d 3445 . . . . . . . 8
234 rneq 5066 . . . . . . . . 9
235234sseq1d 3445 . . . . . . . 8
236231, 233, 2353anbi123d 1365 . . . . . . 7
237234breq1d 4405 . . . . . . . 8
238234eleq1d 2533 . . . . . . . 8
239237, 238anbi12d 725 . . . . . . 7
240236, 239anbi12d 725 . . . . . 6
241124, 240spcev 3127 . . . . 5
2428, 13, 28, 130, 230, 241syl32anc 1300 . . . 4
243242expl 630 . . 3
244243exlimdv 1787 . 2
2456, 244mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904   wne 2641  wral 2756  wrex 2757  crab 2760  cvv 3031   cin 3389   wss 3390  c0 3722  csn 3959  cuni 4190  ciun 4269   class class class wbr 4395   cmpt 4454  ccnv 4838   cdm 4839   crn 4840  cima 4842   wfun 5583   wfn 5584  wf 5585  wfo 5587  cfv 5589   cdom 7585  cfn 7587  ctop 19994  cref 20594  clocfin 20596 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-reg 8125  ax-inf2 8164  ax-ac2 8911 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-er 7381  df-en 7588  df-dom 7589  df-fin 7591  df-r1 8253  df-rank 8254  df-card 8391  df-ac 8565  df-top 19998  df-ref 20597  df-locfin 20599 This theorem is referenced by:  locfinref  28742
 Copyright terms: Public domain W3C validator