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

Theorem txkgen 17362
 Description: The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on can also be replaced with either "comactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015.)
Assertion
Ref Expression
txkgen 𝑛Locally 𝑘Gen 𝑘Gen

Proof of Theorem txkgen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 17215 . . 3 𝑛Locally
2 inss1 3402 . . . . 5 𝑘Gen 𝑘Gen
32sseli 3189 . . . 4 𝑘Gen 𝑘Gen
4 kgentop 17253 . . . 4 𝑘Gen
53, 4syl 15 . . 3 𝑘Gen
6 txtop 17280 . . 3
71, 5, 6syl2an 463 . 2 𝑛Locally 𝑘Gen
8 simplll 734 . . . . . . . 8 𝑛Locally 𝑘Gen 𝑘Gen 𝑛Locally
9 eqid 2296 . . . . . . . . . 10
109mptpreima 5182 . . . . . . . . 9
111ad3antrrr 710 . . . . . . . . . . . . . 14 𝑛Locally 𝑘Gen 𝑘Gen
12 eqid 2296 . . . . . . . . . . . . . . 15
1312toptopon 16687 . . . . . . . . . . . . . 14 TopOn
1411, 13sylib 188 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen TopOn
15 idcn 17003 . . . . . . . . . . . . 13 TopOn
1614, 15syl 15 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen
17 simpllr 735 . . . . . . . . . . . . . . 15 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
1817, 5syl 15 . . . . . . . . . . . . . 14 𝑛Locally 𝑘Gen 𝑘Gen
19 eqid 2296 . . . . . . . . . . . . . . 15
2019toptopon 16687 . . . . . . . . . . . . . 14 TopOn
2118, 20sylib 188 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen TopOn
22 simpr 447 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑘Gen 𝑘Gen
23 simplr 731 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
24 elunii 3848 . . . . . . . . . . . . . . . 16 𝑘Gen 𝑘Gen
2522, 23, 24syl2anc 642 . . . . . . . . . . . . . . 15 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
2612, 19txuni 17303 . . . . . . . . . . . . . . . . 17
2711, 18, 26syl2anc 642 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑘Gen 𝑘Gen
2811, 18, 6syl2anc 642 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑘Gen 𝑘Gen
29 eqid 2296 . . . . . . . . . . . . . . . . . 18
3029kgenuni 17250 . . . . . . . . . . . . . . . . 17 𝑘Gen
3128, 30syl 15 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
3227, 31eqtrd 2328 . . . . . . . . . . . . . . 15 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
3325, 32eleqtrrd 2373 . . . . . . . . . . . . . 14 𝑛Locally 𝑘Gen 𝑘Gen
34 xp2nd 6166 . . . . . . . . . . . . . 14
3533, 34syl 15 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen
36 cnconst2 17027 . . . . . . . . . . . . 13 TopOn TopOn
3714, 21, 35, 36syl3anc 1182 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen
38 fvresi 5727 . . . . . . . . . . . . . . . 16
39 fvex 5555 . . . . . . . . . . . . . . . . 17
4039fvconst2 5745 . . . . . . . . . . . . . . . 16
4138, 40opeq12d 3820 . . . . . . . . . . . . . . 15
4241mpteq2ia 4118 . . . . . . . . . . . . . 14
4342eqcomi 2300 . . . . . . . . . . . . 13
4412, 43txcnmpt 17334 . . . . . . . . . . . 12
4516, 37, 44syl2anc 642 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen
46 llycmpkgen 17263 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen
4746ad3antrrr 710 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
487ad2antrr 706 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen
49 kgencn3 17269 . . . . . . . . . . . 12 𝑘Gen 𝑘Gen
5047, 48, 49syl2anc 642 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
5145, 50eleqtrd 2372 . . . . . . . . . 10 𝑛Locally 𝑘Gen 𝑘Gen 𝑘Gen
52 cnima 17010 . . . . . . . . . 10 𝑘Gen 𝑘Gen
5351, 23, 52syl2anc 642 . . . . . . . . 9 𝑛Locally 𝑘Gen 𝑘Gen
5410, 53syl5eqelr 2381 . . . . . . . 8 𝑛Locally 𝑘Gen 𝑘Gen
55 xp1st 6165 . . . . . . . . . 10
5633, 55syl 15 . . . . . . . . 9 𝑛Locally 𝑘Gen 𝑘Gen
57 1st2nd2 6175 . . . . . . . . . . 11
5833, 57syl 15 . . . . . . . . . 10 𝑛Locally 𝑘Gen 𝑘Gen
5958, 22eqeltrrd 2371 . . . . . . . . 9 𝑛Locally 𝑘Gen 𝑘Gen
60 opeq1 3812 . . . . . . . . . . 11
6160eleq1d 2362 . . . . . . . . . 10
6261elrab 2936 . . . . . . . . 9
6356, 59, 62sylanbrc 645 . . . . . . . 8 𝑛Locally 𝑘Gen 𝑘Gen
64 nlly2i 17218 . . . . . . . 8 𝑛Locally t
658, 54, 63, 64syl3anc 1182 . . . . . . 7 𝑛Locally 𝑘Gen 𝑘Gen t
6611adantr 451 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen t
6718adantr 451 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen t
68 simprlr 739 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen t
69 ssrab2 3271 . . . . . . . . . . . . . 14
7069a1i 10 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen t
71 incom 3374 . . . . . . . . . . . . . . . 16
72 simprll 738 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛Locally 𝑘Gen 𝑘Gen t
73 elpwi 3646 . . . . . . . . . . . . . . . . . . . . . . 23
7472, 73syl 15 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑘Gen 𝑘Gen t
75 ssrab2 3271 . . . . . . . . . . . . . . . . . . . . . 22
7674, 75syl6ss 3204 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑘Gen 𝑘Gen t
7776adantr 451 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑘Gen 𝑘Gen t t
78 elpwi 3646 . . . . . . . . . . . . . . . . . . . . 21
7978ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑘Gen 𝑘Gen t t
80 eldif 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8180anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 anass 630 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8381, 82bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25
8483rexbii2 2585 . . . . . . . . . . . . . . . . . . . . . . . 24
85 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26
86 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8786eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
88 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8988notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9087, 89anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9185, 90syl5bb 248 . . . . . . . . . . . . . . . . . . . . . . . . 25
9291rexxp 4844 . . . . . . . . . . . . . . . . . . . . . . . 24
9384, 92bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23
94 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9594sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9695adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9897sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
99 opelxpi 4737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
10096, 98, 99syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
101 fvres 5558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102100, 101syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
104 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
105103, 104op2nd 6145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
106102, 105syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
107106eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
108107anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
109108rexbidva 2573 . . . . . . . . . . . . . . . . . . . . . . . . . 26
110 opeq2 3813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111110eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112111notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
113112ceqsrexbv 2915 . . . . . . . . . . . . . . . . . . . . . . . . . 26
114109, 113syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . 25
115114rexbidva 2573 . . . . . . . . . . . . . . . . . . . . . . . 24
116 r19.42v 2707 . . . . . . . . . . . . . . . . . . . . . . . 24
117115, 116syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . 23
11893, 117syl5bb 248 . . . . . . . . . . . . . . . . . . . . . 22
119 f2ndres 6158 . . . . . . . . . . . . . . . . . . . . . . . 24
120 ffn 5405 . . . . . . . . . . . . . . . . . . . . . . . 24
121119, 120ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23
122 difss 3316 . . . . . . . . . . . . . . . . . . . . . . . 24
123 xpss12 4808 . . . . . . . . . . . . . . . . . . . . . . . 24
124122, 123syl5ss 3203 . . . . . . . . . . . . . . . . . . . . . . 23
125 fvelimab 5594 . . . . . . . . . . . . . . . . . . . . . . 23
126121, 124, 125sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22
127 eldif 3175 . . . . . . . . . . . . . . . . . . . . . . 23
128 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
129128sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
130 sneq 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
131130xpeq2d 4729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132131sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
133 dfss3 3183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
135134ralxp 4843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
136 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
137 opeq2 3813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
138137eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
139136, 138ralsn 3687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
140139ralbii 2580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141133, 135, 1403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142132, 141syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143142elrab3 2937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
144129, 143syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26
145144notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . 25
146 rexnal 2567 . . . . . . . . . . . . . . . . . . . . . . . . 25
147145, 146syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . . . 24
148147pm5.32da 622 . . . . . . . . . . . . . . . . . . . . . . 23
149127, 148syl5bb 248 . . . . . . . . . . . . . . . . . . . . . 22
150118, 126, 1493bitr4d 276 . . . . . . . . . . . . . . . . . . . . 21
151150eqrdv 2294 . . . . . . . . . . . . . . . . . . . 20
15277, 79, 151syl2anc 642 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑘Gen 𝑘Gen t t
153 difin 3419 . . . . . . . . . . . . . . . . . . . 20
15467adantr 451 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑘Gen 𝑘Gen t t
15519restuni 16909 . . . . . . . . . . . . . . . . . . . . . 22 t
156154, 79, 155syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑘Gen 𝑘Gen t t t
157156difeq1d 3306 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑘Gen 𝑘Gen t t t
158153, 157syl5eqr 2342 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑘Gen 𝑘Gen t t t
159152, 158eqtrd 2328 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑘Gen 𝑘Gen t t t
160 inss2 3403 . . . . . . . . . . . . . . . . . . . . 21 𝑘Gen
16117ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑘Gen 𝑘Gen t t 𝑘Gen
162160, 161sseldi 3191 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑘Gen 𝑘Gen t t
163 df-ima 4718 . . . . . . . . . . . . . . . . . . . . . . 23
164 resres 4984 . . . . . . . . . . . . . . . . . . . . . . . . 25
165 inss2 3403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
166165, 122sstri 3201 . . . . . . . . . . . . . . . . . . . . . . . . . 26
167 ssres2 4998 . . . . . . . . . . . . . . . . . . . . . . . . . 26
168166, 167ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . 25
169164, 168eqsstri 3221 . . . . . . . . . . . . . . . . . . . . . . . 24
170 rnss 4923 . . . . . . . . . . . . . . . . . . . . . . . 24
171169, 170ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23
172163, 171eqsstri 3221 . . . . . . . . . . . . . . . . . . . . . 22
173 f2ndres 6158 . . . . . . . . . . . . . . . . . . . . . . 23
174 frn 5411 . . . . . . . . . . . . . . . . . . . . . . 23
175173, 174ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22
176172, 175sstri 3201 . . . . . . . . . . . . . . . . . . . . 21
177176, 79syl5ss 3203 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑘Gen 𝑘Gen t t
17814ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑘Gen 𝑘Gen t t TopOn
179154, 20sylib 188 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑘Gen 𝑘Gen t t TopOn
180 tx2cn 17320 . . . . . . . . . . . . . . . . . . . . . 22 TopOn TopOn
181178, 179, 180syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑘Gen 𝑘Gen t t
18228ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛Locally 𝑘Gen 𝑘Gen t t
183122a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛Locally 𝑘Gen 𝑘Gen t t
184 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . 25
185 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . 25
186184, 185xpex 4817 . . . . . . . . . . . . . . . . . . . . . . . 24
187186a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛Locally 𝑘Gen 𝑘Gen t t
188 restabs 16912 . . . . . . . . . . . . . . . . . . . . . . 23 t t t
189182, 183, 187, 188syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑘Gen 𝑘Gen t t t t t
19066adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t
191161, 5syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t
192184a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t
193 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t
194 txrest 17341 . . . . . . . . . . . . . . . . . . . . . . . . 25 t t t
195190, 191, 192, 193, 194syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛Locally 𝑘Gen 𝑘Gen t t t t t
196 simprr3 1005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛Locally 𝑘Gen 𝑘Gen t t
197196adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t t
198 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t t
199 txcmp 17353 . . . . . . . . . . . . . . . . . . . . . . . . 25 t t t t
200197, 198, 199syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛Locally 𝑘Gen 𝑘Gen t t t t
201195, 200eqeltrd 2370 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛Locally 𝑘Gen 𝑘Gen t t t
202 difin 3419 . . . . . . . . . . . . . . . . . . . . . . . . 25
20377, 79, 123syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛Locally 𝑘Gen 𝑘Gen t t
204190, 154, 26syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛Locally 𝑘Gen 𝑘Gen t t
205203, 204sseqtrd 3227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛Locally 𝑘Gen 𝑘Gen t t
20629restuni 16909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 t
207182, 205, 206syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛Locally 𝑘Gen 𝑘Gen t t t
208207difeq1d 3306 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t t
209202, 208syl5eqr 2342 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛Locally 𝑘Gen 𝑘Gen t t t
210 resttop 16907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 t
211182, 186, 210sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t t
212 incom 3374 . . . . . . . . . . . . . . . . . . . . . . . . . 26
21323ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛Locally 𝑘Gen 𝑘Gen t t 𝑘Gen
214 kgeni 17248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑘Gen t t
215213, 201, 214syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛Locally 𝑘Gen 𝑘Gen t t t
216212, 215syl5eqel 2380 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛Locally 𝑘Gen 𝑘Gen t t t
217 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . 26 t t
218217opncld 16786 . . . . . . . . . . . . . . . . . . . . . . . . 25 t t t t
219211, 216, 218syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛Locally 𝑘Gen 𝑘Gen t t t t
220209, 219eqeltrd 2370 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛Locally 𝑘Gen 𝑘Gen t t t
221 cmpcld 17145 . . . . . . . . . . . . . . . . . . . . . . 23 t t t t
222201, 220, 221syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑘Gen 𝑘Gen t t t t
223189, 222eqeltrrd 2371 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑘Gen 𝑘Gen t t t
224 imacmp 17140 . . . . . . . . . . . . . . . . . . . . 21 t t
225181, 223, 224syl2anc 642 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑘Gen 𝑘Gen t t t
22619hauscmp 17150 . . . . . . . . . . . . . . . . . . . 20 t
227162, 177, 225, 226syl3anc 1182 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑘Gen 𝑘Gen t t
228176a1i 10 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑘Gen 𝑘Gen t t
22919restcldi 16920 . . . . . . . . . . . . . . . . . . 19 t
23079, 227, 228, 229syl3anc 1182 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑘Gen 𝑘Gen t t t
231159, 230eqeltrrd 2371 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑘Gen 𝑘Gen t t t t
232 resttop 16907 . . . . . . . . . . . . . . . . . . 19 t
233154, 193, 232syl2anc 642 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑘Gen 𝑘Gen t t t
234 inss1 3402 . . . . . . . . . . . . . . . . . . 19
235234, 156syl5sseq 3239 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑘Gen 𝑘Gen t t t
236 eqid 2296 . . . . . . . . . . . . . . . . . . 19 t t
237236isopn2 16785 . . . . . . . . . . . . . . . . . 18 t t t t t
238233, 235, 237syl2anc 642 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑘Gen 𝑘Gen t t t t t
239231, 238mpbird 223 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑘Gen 𝑘Gen t t t
24071, 239syl5eqel 2380 . . . . . . . . . . . . . . 15 𝑛Locally 𝑘Gen 𝑘Gen t t t
241240expr 598 . . . . . . . . . . . . . 14 𝑛Locally 𝑘Gen 𝑘Gen t t t
242241ralrimiva 2639 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen t t t
24367, 20sylib 188 . . . . . . . . . . . . . 14 𝑛Locally 𝑘Gen 𝑘Gen t TopOn
244 elkgen 17247 . . . . . . . . . . . . . 14 TopOn 𝑘Gen t t
245243, 244syl 15 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen t 𝑘Gen t t
24670, 242, 245mpbir2and 888 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen t 𝑘Gen
24717adantr 451 . . . . . . . . . . . . . 14 𝑛Locally 𝑘Gen 𝑘Gen t 𝑘Gen
248247, 3syl 15 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen t 𝑘Gen
249 kgenidm 17258 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen
250248, 249syl 15 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen t 𝑘Gen
251246, 250eleqtrd 2372 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen t
252 txopn 17313 . . . . . . . . . . 11
25366, 67, 68, 251, 252syl22anc 1183 . . . . . . . . . 10 𝑛Locally 𝑘Gen 𝑘Gen t
25458adantr 451 . . . . . . . . . . 11 𝑛Locally 𝑘Gen 𝑘Gen t
255 simprr1 1003 . . . . . . . . . . . 12 𝑛Locally 𝑘Gen 𝑘Gen t
25635adantr 451 . . . . . . . . . . . . 13 𝑛Locally 𝑘Gen 𝑘Gen t
257 relxp 4810 . . . . . . . . . . . . . . 15
258257a1i 10 . . . . . . . . . . . . . 14