Metamath Proof Explorer


Theorem txkgen

Description: The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on S can also be replaced with either "compactly 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)

Ref Expression
Assertion txkgen R N-Locally Comp S ran 𝑘Gen Haus R × t S ran 𝑘Gen

Proof

Step Hyp Ref Expression
1 nllytop R N-Locally Comp R Top
2 elinel1 S ran 𝑘Gen Haus S ran 𝑘Gen
3 kgentop S ran 𝑘Gen S Top
4 2 3 syl S ran 𝑘Gen Haus S Top
5 txtop R Top S Top R × t S Top
6 1 4 5 syl2an R N-Locally Comp S ran 𝑘Gen Haus R × t S Top
7 simplll R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R N-Locally Comp
8 eqid t R t 2 nd y = t R t 2 nd y
9 8 mptpreima t R t 2 nd y -1 x = t R | t 2 nd y x
10 1 ad3antrrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R Top
11 toptopon2 R Top R TopOn R
12 10 11 sylib R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R TopOn R
13 idcn R TopOn R I R R Cn R
14 12 13 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x I R R Cn R
15 simpllr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x S ran 𝑘Gen Haus
16 15 4 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x S Top
17 toptopon2 S Top S TopOn S
18 16 17 sylib R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x S TopOn S
19 simpr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x y x
20 simplr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x x 𝑘Gen R × t S
21 elunii y x x 𝑘Gen R × t S y 𝑘Gen R × t S
22 19 20 21 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x y 𝑘Gen R × t S
23 eqid R = R
24 eqid S = S
25 23 24 txuni R Top S Top R × S = R × t S
26 10 16 25 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R × S = R × t S
27 10 16 5 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R × t S Top
28 eqid R × t S = R × t S
29 28 kgenuni R × t S Top R × t S = 𝑘Gen R × t S
30 27 29 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R × t S = 𝑘Gen R × t S
31 26 30 eqtrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R × S = 𝑘Gen R × t S
32 22 31 eleqtrrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x y R × S
33 xp2nd y R × S 2 nd y S
34 32 33 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x 2 nd y S
35 cnconst2 R TopOn R S TopOn S 2 nd y S R × 2 nd y R Cn S
36 12 18 34 35 syl3anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R × 2 nd y R Cn S
37 fvresi t R I R t = t
38 fvex 2 nd y V
39 38 fvconst2 t R R × 2 nd y t = 2 nd y
40 37 39 opeq12d t R I R t R × 2 nd y t = t 2 nd y
41 40 mpteq2ia t R I R t R × 2 nd y t = t R t 2 nd y
42 41 eqcomi t R t 2 nd y = t R I R t R × 2 nd y t
43 23 42 txcnmpt I R R Cn R R × 2 nd y R Cn S t R t 2 nd y R Cn R × t S
44 14 36 43 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x t R t 2 nd y R Cn R × t S
45 llycmpkgen R N-Locally Comp R ran 𝑘Gen
46 45 ad3antrrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R ran 𝑘Gen
47 6 ad2antrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R × t S Top
48 kgencn3 R ran 𝑘Gen R × t S Top R Cn R × t S = R Cn 𝑘Gen R × t S
49 46 47 48 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x R Cn R × t S = R Cn 𝑘Gen R × t S
50 44 49 eleqtrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x t R t 2 nd y R Cn 𝑘Gen R × t S
51 cnima t R t 2 nd y R Cn 𝑘Gen R × t S x 𝑘Gen R × t S t R t 2 nd y -1 x R
52 50 20 51 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x t R t 2 nd y -1 x R
53 9 52 eqeltrrid R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x t R | t 2 nd y x R
54 opeq1 t = 1 st y t 2 nd y = 1 st y 2 nd y
55 54 eleq1d t = 1 st y t 2 nd y x 1 st y 2 nd y x
56 xp1st y R × S 1 st y R
57 32 56 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x 1 st y R
58 1st2nd2 y R × S y = 1 st y 2 nd y
59 32 58 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x y = 1 st y 2 nd y
60 59 19 eqeltrrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x 1 st y 2 nd y x
61 55 57 60 elrabd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x 1 st y t R | t 2 nd y x
62 nlly2i R N-Locally Comp t R | t 2 nd y x R 1 st y t R | t 2 nd y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp
63 7 53 61 62 syl3anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp
64 10 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp R Top
65 16 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp S Top
66 simprlr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp u R
67 ssrab2 v S | s × v x S
68 67 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp v S | s × v x S
69 incom v S | s × v x k = k v S | s × v x
70 simprll R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp s 𝒫 t R | t 2 nd y x
71 70 elpwid R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp s t R | t 2 nd y x
72 ssrab2 t R | t 2 nd y x R
73 71 72 sstrdi R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp s R
74 73 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s R
75 elpwi k 𝒫 S k S
76 75 ad2antrl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k S
77 eldif t s × k x t s × k ¬ t x
78 77 anbi1i t s × k x 2 nd R × S t = b t s × k ¬ t x 2 nd R × S t = b
79 anass t s × k ¬ t x 2 nd R × S t = b t s × k ¬ t x 2 nd R × S t = b
80 78 79 bitri t s × k x 2 nd R × S t = b t s × k ¬ t x 2 nd R × S t = b
81 80 rexbii2 t s × k x 2 nd R × S t = b t s × k ¬ t x 2 nd R × S t = b
82 ancom ¬ t x 2 nd R × S t = b 2 nd R × S t = b ¬ t x
83 fveqeq2 t = a u 2 nd R × S t = b 2 nd R × S a u = b
84 eleq1 t = a u t x a u x
85 84 notbid t = a u ¬ t x ¬ a u x
86 83 85 anbi12d t = a u 2 nd R × S t = b ¬ t x 2 nd R × S a u = b ¬ a u x
87 82 86 syl5bb t = a u ¬ t x 2 nd R × S t = b 2 nd R × S a u = b ¬ a u x
88 87 rexxp t s × k ¬ t x 2 nd R × S t = b a s u k 2 nd R × S a u = b ¬ a u x
89 81 88 bitri t s × k x 2 nd R × S t = b a s u k 2 nd R × S a u = b ¬ a u x
90 simpl s R k S s R
91 90 sselda s R k S a s a R
92 91 adantr s R k S a s u k a R
93 simplr s R k S a s k S
94 93 sselda s R k S a s u k u S
95 92 94 opelxpd s R k S a s u k a u R × S
96 95 fvresd s R k S a s u k 2 nd R × S a u = 2 nd a u
97 vex a V
98 vex u V
99 97 98 op2nd 2 nd a u = u
100 96 99 eqtrdi s R k S a s u k 2 nd R × S a u = u
101 100 eqeq1d s R k S a s u k 2 nd R × S a u = b u = b
102 101 anbi1d s R k S a s u k 2 nd R × S a u = b ¬ a u x u = b ¬ a u x
103 102 rexbidva s R k S a s u k 2 nd R × S a u = b ¬ a u x u k u = b ¬ a u x
104 opeq2 u = b a u = a b
105 104 eleq1d u = b a u x a b x
106 105 notbid u = b ¬ a u x ¬ a b x
107 106 ceqsrexbv u k u = b ¬ a u x b k ¬ a b x
108 103 107 bitrdi s R k S a s u k 2 nd R × S a u = b ¬ a u x b k ¬ a b x
109 108 rexbidva s R k S a s u k 2 nd R × S a u = b ¬ a u x a s b k ¬ a b x
110 r19.42v a s b k ¬ a b x b k a s ¬ a b x
111 109 110 bitrdi s R k S a s u k 2 nd R × S a u = b ¬ a u x b k a s ¬ a b x
112 89 111 syl5bb s R k S t s × k x 2 nd R × S t = b b k a s ¬ a b x
113 f2ndres 2 nd R × S : R × S S
114 ffn 2 nd R × S : R × S S 2 nd R × S Fn R × S
115 113 114 ax-mp 2 nd R × S Fn R × S
116 difss s × k x s × k
117 xpss12 s R k S s × k R × S
118 116 117 sstrid s R k S s × k x R × S
119 fvelimab 2 nd R × S Fn R × S s × k x R × S b 2 nd R × S s × k x t s × k x 2 nd R × S t = b
120 115 118 119 sylancr s R k S b 2 nd R × S s × k x t s × k x 2 nd R × S t = b
121 eldif b k v S | s × v x b k ¬ b v S | s × v x
122 simpr s R k S k S
123 122 sselda s R k S b k b S
124 sneq v = b v = b
125 124 xpeq2d v = b s × v = s × b
126 125 sseq1d v = b s × v x s × b x
127 dfss3 s × b x k s × b k x
128 eleq1 k = a t k x a t x
129 128 ralxp k s × b k x a s t b a t x
130 vex b V
131 opeq2 t = b a t = a b
132 131 eleq1d t = b a t x a b x
133 130 132 ralsn t b a t x a b x
134 133 ralbii a s t b a t x a s a b x
135 127 129 134 3bitri s × b x a s a b x
136 126 135 bitrdi v = b s × v x a s a b x
137 136 elrab3 b S b v S | s × v x a s a b x
138 123 137 syl s R k S b k b v S | s × v x a s a b x
139 138 notbid s R k S b k ¬ b v S | s × v x ¬ a s a b x
140 rexnal a s ¬ a b x ¬ a s a b x
141 139 140 bitr4di s R k S b k ¬ b v S | s × v x a s ¬ a b x
142 141 pm5.32da s R k S b k ¬ b v S | s × v x b k a s ¬ a b x
143 121 142 syl5bb s R k S b k v S | s × v x b k a s ¬ a b x
144 112 120 143 3bitr4d s R k S b 2 nd R × S s × k x b k v S | s × v x
145 144 eqrdv s R k S 2 nd R × S s × k x = k v S | s × v x
146 74 76 145 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S s × k x = k v S | s × v x
147 difin k k v S | s × v x = k v S | s × v x
148 65 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S Top
149 24 restuni S Top k S k = S 𝑡 k
150 148 76 149 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k = S 𝑡 k
151 150 difeq1d R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k k v S | s × v x = S 𝑡 k k v S | s × v x
152 147 151 eqtr3id R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k v S | s × v x = S 𝑡 k k v S | s × v x
153 146 152 eqtrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S s × k x = S 𝑡 k k v S | s × v x
154 15 ad2antrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S ran 𝑘Gen Haus
155 154 elin2d R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S Haus
156 df-ima 2 nd R × S s × k x = ran 2 nd R × S s × k x
157 resres 2 nd R × S s × k x = 2 nd R × S s × k x
158 inss2 R × S s × k x s × k x
159 158 116 sstri R × S s × k x s × k
160 ssres2 R × S s × k x s × k 2 nd R × S s × k x 2 nd s × k
161 159 160 ax-mp 2 nd R × S s × k x 2 nd s × k
162 157 161 eqsstri 2 nd R × S s × k x 2 nd s × k
163 162 rnssi ran 2 nd R × S s × k x ran 2 nd s × k
164 156 163 eqsstri 2 nd R × S s × k x ran 2 nd s × k
165 f2ndres 2 nd s × k : s × k k
166 frn 2 nd s × k : s × k k ran 2 nd s × k k
167 165 166 ax-mp ran 2 nd s × k k
168 164 167 sstri 2 nd R × S s × k x k
169 168 76 sstrid R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S s × k x S
170 12 ad2antrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R TopOn R
171 148 17 sylib R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S TopOn S
172 tx2cn R TopOn R S TopOn S 2 nd R × S R × t S Cn S
173 170 171 172 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S R × t S Cn S
174 27 ad2antrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S Top
175 116 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k x s × k
176 vex s V
177 vex k V
178 176 177 xpex s × k V
179 178 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k V
180 restabs R × t S Top s × k x s × k s × k V R × t S 𝑡 s × k 𝑡 s × k x = R × t S 𝑡 s × k x
181 174 175 179 180 syl3anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k 𝑡 s × k x = R × t S 𝑡 s × k x
182 64 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R Top
183 154 4 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S Top
184 176 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s V
185 simprl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k 𝒫 S
186 txrest R Top S Top s V k 𝒫 S R × t S 𝑡 s × k = R 𝑡 s × t S 𝑡 k
187 182 183 184 185 186 syl22anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k = R 𝑡 s × t S 𝑡 k
188 simprr3 R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp R 𝑡 s Comp
189 188 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R 𝑡 s Comp
190 simprr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S 𝑡 k Comp
191 txcmp R 𝑡 s Comp S 𝑡 k Comp R 𝑡 s × t S 𝑡 k Comp
192 189 190 191 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R 𝑡 s × t S 𝑡 k Comp
193 187 192 eqeltrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k Comp
194 difin s × k s × k x = s × k x
195 74 76 117 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k R × S
196 182 148 25 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × S = R × t S
197 195 196 sseqtrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k R × t S
198 28 restuni R × t S Top s × k R × t S s × k = R × t S 𝑡 s × k
199 174 197 198 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k = R × t S 𝑡 s × k
200 199 difeq1d R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k s × k x = R × t S 𝑡 s × k s × k x
201 194 200 eqtr3id R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k x = R × t S 𝑡 s × k s × k x
202 resttop R × t S Top s × k V R × t S 𝑡 s × k Top
203 174 178 202 sylancl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k Top
204 incom s × k x = x s × k
205 20 ad2antrr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp x 𝑘Gen R × t S
206 kgeni x 𝑘Gen R × t S R × t S 𝑡 s × k Comp x s × k R × t S 𝑡 s × k
207 205 193 206 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp x s × k R × t S 𝑡 s × k
208 204 207 eqeltrid R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k x R × t S 𝑡 s × k
209 eqid R × t S 𝑡 s × k = R × t S 𝑡 s × k
210 209 opncld R × t S 𝑡 s × k Top s × k x R × t S 𝑡 s × k R × t S 𝑡 s × k s × k x Clsd R × t S 𝑡 s × k
211 203 208 210 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k s × k x Clsd R × t S 𝑡 s × k
212 201 211 eqeltrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp s × k x Clsd R × t S 𝑡 s × k
213 cmpcld R × t S 𝑡 s × k Comp s × k x Clsd R × t S 𝑡 s × k R × t S 𝑡 s × k 𝑡 s × k x Comp
214 193 212 213 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k 𝑡 s × k x Comp
215 181 214 eqeltrrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp R × t S 𝑡 s × k x Comp
216 imacmp 2 nd R × S R × t S Cn S R × t S 𝑡 s × k x Comp S 𝑡 2 nd R × S s × k x Comp
217 173 215 216 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S 𝑡 2 nd R × S s × k x Comp
218 24 hauscmp S Haus 2 nd R × S s × k x S S 𝑡 2 nd R × S s × k x Comp 2 nd R × S s × k x Clsd S
219 155 169 217 218 syl3anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S s × k x Clsd S
220 168 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S s × k x k
221 24 restcldi k S 2 nd R × S s × k x Clsd S 2 nd R × S s × k x k 2 nd R × S s × k x Clsd S 𝑡 k
222 76 219 220 221 syl3anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp 2 nd R × S s × k x Clsd S 𝑡 k
223 153 222 eqeltrrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S 𝑡 k k v S | s × v x Clsd S 𝑡 k
224 resttop S Top k 𝒫 S S 𝑡 k Top
225 148 185 224 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp S 𝑡 k Top
226 inss1 k v S | s × v x k
227 226 150 sseqtrid R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k v S | s × v x S 𝑡 k
228 eqid S 𝑡 k = S 𝑡 k
229 228 isopn2 S 𝑡 k Top k v S | s × v x S 𝑡 k k v S | s × v x S 𝑡 k S 𝑡 k k v S | s × v x Clsd S 𝑡 k
230 225 227 229 syl2anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k v S | s × v x S 𝑡 k S 𝑡 k k v S | s × v x Clsd S 𝑡 k
231 223 230 mpbird R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp k v S | s × v x S 𝑡 k
232 69 231 eqeltrid R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp v S | s × v x k S 𝑡 k
233 232 expr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp v S | s × v x k S 𝑡 k
234 233 ralrimiva R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp k 𝒫 S S 𝑡 k Comp v S | s × v x k S 𝑡 k
235 65 17 sylib R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp S TopOn S
236 elkgen S TopOn S v S | s × v x 𝑘Gen S v S | s × v x S k 𝒫 S S 𝑡 k Comp v S | s × v x k S 𝑡 k
237 235 236 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp v S | s × v x 𝑘Gen S v S | s × v x S k 𝒫 S S 𝑡 k Comp v S | s × v x k S 𝑡 k
238 68 234 237 mpbir2and R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp v S | s × v x 𝑘Gen S
239 15 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp S ran 𝑘Gen Haus
240 239 2 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp S ran 𝑘Gen
241 kgenidm S ran 𝑘Gen 𝑘Gen S = S
242 240 241 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp 𝑘Gen S = S
243 238 242 eleqtrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp v S | s × v x S
244 txopn R Top S Top u R v S | s × v x S u × v S | s × v x R × t S
245 64 65 66 243 244 syl22anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp u × v S | s × v x R × t S
246 59 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp y = 1 st y 2 nd y
247 simprr1 R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp 1 st y u
248 sneq v = 2 nd y v = 2 nd y
249 248 xpeq2d v = 2 nd y s × v = s × 2 nd y
250 249 sseq1d v = 2 nd y s × v x s × 2 nd y x
251 34 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp 2 nd y S
252 relxp Rel s × 2 nd y
253 252 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp Rel s × 2 nd y
254 opelxp a b s × 2 nd y a s b 2 nd y
255 71 sselda R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a s a t R | t 2 nd y x
256 opeq1 t = a t 2 nd y = a 2 nd y
257 256 eleq1d t = a t 2 nd y x a 2 nd y x
258 257 elrab a t R | t 2 nd y x a R a 2 nd y x
259 258 simprbi a t R | t 2 nd y x a 2 nd y x
260 255 259 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a s a 2 nd y x
261 elsni b 2 nd y b = 2 nd y
262 261 opeq2d b 2 nd y a b = a 2 nd y
263 262 eleq1d b 2 nd y a b x a 2 nd y x
264 260 263 syl5ibrcom R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a s b 2 nd y a b x
265 264 expimpd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a s b 2 nd y a b x
266 254 265 syl5bi R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a b s × 2 nd y a b x
267 253 266 relssdv R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp s × 2 nd y x
268 250 251 267 elrabd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp 2 nd y v S | s × v x
269 247 268 opelxpd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp 1 st y 2 nd y u × v S | s × v x
270 246 269 eqeltrd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp y u × v S | s × v x
271 relxp Rel u × v S | s × v x
272 271 a1i R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp Rel u × v S | s × v x
273 opelxp a b u × v S | s × v x a u b v S | s × v x
274 126 elrab b v S | s × v x b S s × b x
275 274 simprbi b v S | s × v x s × b x
276 simprr2 R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp u s
277 276 sselda R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a u a s
278 vsnid b b
279 opelxpi a s b b a b s × b
280 277 278 279 sylancl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a u a b s × b
281 ssel s × b x a b s × b a b x
282 275 280 281 syl2imc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a u b v S | s × v x a b x
283 282 expimpd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a u b v S | s × v x a b x
284 273 283 syl5bi R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp a b u × v S | s × v x a b x
285 272 284 relssdv R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp u × v S | s × v x x
286 eleq2 t = u × v S | s × v x y t y u × v S | s × v x
287 sseq1 t = u × v S | s × v x t x u × v S | s × v x x
288 286 287 anbi12d t = u × v S | s × v x y t t x y u × v S | s × v x u × v S | s × v x x
289 288 rspcev u × v S | s × v x R × t S y u × v S | s × v x u × v S | s × v x x t R × t S y t t x
290 245 270 285 289 syl12anc R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp t R × t S y t t x
291 290 expr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp t R × t S y t t x
292 291 rexlimdvva R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x s 𝒫 t R | t 2 nd y x u R 1 st y u u s R 𝑡 s Comp t R × t S y t t x
293 63 292 mpd R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x t R × t S y t t x
294 293 ralrimiva R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S y x t R × t S y t t x
295 6 adantr R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S R × t S Top
296 eltop2 R × t S Top x R × t S y x t R × t S y t t x
297 295 296 syl R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S x R × t S y x t R × t S y t t x
298 294 297 mpbird R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S x R × t S
299 298 ex R N-Locally Comp S ran 𝑘Gen Haus x 𝑘Gen R × t S x R × t S
300 299 ssrdv R N-Locally Comp S ran 𝑘Gen Haus 𝑘Gen R × t S R × t S
301 iskgen2 R × t S ran 𝑘Gen R × t S Top 𝑘Gen R × t S R × t S
302 6 300 301 sylanbrc R N-Locally Comp S ran 𝑘Gen Haus R × t S ran 𝑘Gen