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

Theorem txkgen 17346
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 "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  |-  ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  -> 
( R  tX  S
)  e.  ran 𝑘Gen )

Proof of Theorem txkgen
Dummy variables  a 
b  k  s  t  u  x  y  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 17199 . . 3  |-  ( R  e. 𝑛Locally 
Comp  ->  R  e.  Top )
2 inss1 3389 . . . . 5  |-  ( ran 𝑘Gen  i^i 
Haus )  C_  ran 𝑘Gen
32sseli 3176 . . . 4  |-  ( S  e.  ( ran 𝑘Gen  i^i  Haus )  ->  S  e.  ran 𝑘Gen )
4 kgentop 17237 . . . 4  |-  ( S  e.  ran 𝑘Gen  ->  S  e.  Top )
53, 4syl 15 . . 3  |-  ( S  e.  ( ran 𝑘Gen  i^i  Haus )  ->  S  e.  Top )
6 txtop 17264 . . 3  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( R  tX  S
)  e.  Top )
71, 5, 6syl2an 463 . 2  |-  ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  -> 
( R  tX  S
)  e.  Top )
8 simplll 734 . . . . . . . 8  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  R  e. 𝑛Locally  Comp )
9 eqid 2283 . . . . . . . . . 10  |-  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )  =  ( t  e. 
U. R  |->  <. t ,  ( 2nd `  y
) >. )
109mptpreima 5166 . . . . . . . . 9  |-  ( `' ( t  e.  U. R  |->  <. t ,  ( 2nd `  y )
>. ) " x )  =  { t  e. 
U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }
111ad3antrrr 710 . . . . . . . . . . . . . 14  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  R  e.  Top )
12 eqid 2283 . . . . . . . . . . . . . . 15  |-  U. R  =  U. R
1312toptopon 16671 . . . . . . . . . . . . . 14  |-  ( R  e.  Top  <->  R  e.  (TopOn `  U. R ) )
1411, 13sylib 188 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  R  e.  (TopOn `  U. R ) )
15 idcn 16987 . . . . . . . . . . . . 13  |-  ( R  e.  (TopOn `  U. R )  ->  (  _I  |`  U. R )  e.  ( R  Cn  R ) )
1614, 15syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  (  _I  |`  U. R )  e.  ( R  Cn  R ) )
17 simpllr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  S  e.  ( ran 𝑘Gen  i^i  Haus )
)
1817, 5syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  S  e.  Top )
19 eqid 2283 . . . . . . . . . . . . . . 15  |-  U. S  =  U. S
2019toptopon 16671 . . . . . . . . . . . . . 14  |-  ( S  e.  Top  <->  S  e.  (TopOn `  U. S ) )
2118, 20sylib 188 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  S  e.  (TopOn `  U. S ) )
22 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  y  e.  x )
23 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  x  e.  (𝑘Gen `  ( R  tX  S ) ) )
24 elunii 3832 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  x  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  ->  y  e.  U. (𝑘Gen `  ( R  tX  S ) ) )
2522, 23, 24syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  y  e.  U. (𝑘Gen `  ( R  tX  S ) ) )
2612, 19txuni 17287 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( U. R  X.  U. S )  =  U. ( R  tX  S ) )
2711, 18, 26syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( U. R  X.  U. S
)  =  U. ( R  tX  S ) )
2811, 18, 6syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( R  tX  S )  e. 
Top )
29 eqid 2283 . . . . . . . . . . . . . . . . . 18  |-  U. ( R  tX  S )  = 
U. ( R  tX  S )
3029kgenuni 17234 . . . . . . . . . . . . . . . . 17  |-  ( ( R  tX  S )  e.  Top  ->  U. ( R  tX  S )  = 
U. (𝑘Gen `  ( R  tX  S ) ) )
3128, 30syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  U. ( R  tX  S )  = 
U. (𝑘Gen `  ( R  tX  S ) ) )
3227, 31eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( U. R  X.  U. S
)  =  U. (𝑘Gen `  ( R  tX  S ) ) )
3325, 32eleqtrrd 2360 . . . . . . . . . . . . . 14  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  y  e.  ( U. R  X.  U. S ) )
34 xp2nd 6150 . . . . . . . . . . . . . 14  |-  ( y  e.  ( U. R  X.  U. S )  -> 
( 2nd `  y
)  e.  U. S
)
3533, 34syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( 2nd `  y )  e. 
U. S )
36 cnconst2 17011 . . . . . . . . . . . . 13  |-  ( ( R  e.  (TopOn `  U. R )  /\  S  e.  (TopOn `  U. S )  /\  ( 2nd `  y
)  e.  U. S
)  ->  ( U. R  X.  { ( 2nd `  y ) } )  e.  ( R  Cn  S ) )
3714, 21, 35, 36syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( U. R  X.  { ( 2nd `  y ) } )  e.  ( R  Cn  S ) )
38 fvresi 5711 . . . . . . . . . . . . . . . 16  |-  ( t  e.  U. R  -> 
( (  _I  |`  U. R
) `  t )  =  t )
39 fvex 5539 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  y )  e.  _V
4039fvconst2 5729 . . . . . . . . . . . . . . . 16  |-  ( t  e.  U. R  -> 
( ( U. R  X.  { ( 2nd `  y
) } ) `  t )  =  ( 2nd `  y ) )
4138, 40opeq12d 3804 . . . . . . . . . . . . . . 15  |-  ( t  e.  U. R  ->  <. ( (  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.  =  <. t ,  ( 2nd `  y )
>. )
4241mpteq2ia 4102 . . . . . . . . . . . . . 14  |-  ( t  e.  U. R  |->  <.
( (  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.
)  =  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )
4342eqcomi 2287 . . . . . . . . . . . . 13  |-  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )  =  ( t  e. 
U. R  |->  <. (
(  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.
)
4412, 43txcnmpt 17318 . . . . . . . . . . . 12  |-  ( ( (  _I  |`  U. R
)  e.  ( R  Cn  R )  /\  ( U. R  X.  {
( 2nd `  y
) } )  e.  ( R  Cn  S
) )  ->  (
t  e.  U. R  |-> 
<. t ,  ( 2nd `  y ) >. )  e.  ( R  Cn  ( R  tX  S ) ) )
4516, 37, 44syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  (
t  e.  U. R  |-> 
<. t ,  ( 2nd `  y ) >. )  e.  ( R  Cn  ( R  tX  S ) ) )
46 llycmpkgen 17247 . . . . . . . . . . . . 13  |-  ( R  e. 𝑛Locally 
Comp  ->  R  e.  ran 𝑘Gen )
4746ad3antrrr 710 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  R  e.  ran 𝑘Gen )
487ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( R  tX  S )  e. 
Top )
49 kgencn3 17253 . . . . . . . . . . . 12  |-  ( ( R  e.  ran 𝑘Gen  /\  ( R  tX  S )  e. 
Top )  ->  ( R  Cn  ( R  tX  S ) )  =  ( R  Cn  (𝑘Gen `  ( R  tX  S ) ) ) )
5047, 48, 49syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( R  Cn  ( R  tX  S ) )  =  ( R  Cn  (𝑘Gen `  ( R  tX  S ) ) ) )
5145, 50eleqtrd 2359 . . . . . . . . . 10  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  (
t  e.  U. R  |-> 
<. t ,  ( 2nd `  y ) >. )  e.  ( R  Cn  (𝑘Gen `  ( R  tX  S ) ) ) )
52 cnima 16994 . . . . . . . . . 10  |-  ( ( ( t  e.  U. R  |->  <. t ,  ( 2nd `  y )
>. )  e.  ( R  Cn  (𝑘Gen `  ( R  tX  S ) ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S
) ) )  -> 
( `' ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. ) " x )  e.  R )
5351, 23, 52syl2anc 642 . . . . . . . . 9  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( `' ( t  e. 
U. R  |->  <. t ,  ( 2nd `  y
) >. ) " x
)  e.  R )
5410, 53syl5eqelr 2368 . . . . . . . 8  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x }  e.  R )
55 xp1st 6149 . . . . . . . . . 10  |-  ( y  e.  ( U. R  X.  U. S )  -> 
( 1st `  y
)  e.  U. R
)
5633, 55syl 15 . . . . . . . . 9  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( 1st `  y )  e. 
U. R )
57 1st2nd2 6159 . . . . . . . . . . 11  |-  ( y  e.  ( U. R  X.  U. S )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
5833, 57syl 15 . . . . . . . . . 10  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
5958, 22eqeltrrd 2358 . . . . . . . . 9  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  e.  x )
60 opeq1 3796 . . . . . . . . . . 11  |-  ( t  =  ( 1st `  y
)  ->  <. t ,  ( 2nd `  y
) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
6160eleq1d 2349 . . . . . . . . . 10  |-  ( t  =  ( 1st `  y
)  ->  ( <. t ,  ( 2nd `  y
) >.  e.  x  <->  <. ( 1st `  y ) ,  ( 2nd `  y )
>.  e.  x ) )
6261elrab 2923 . . . . . . . . 9  |-  ( ( 1st `  y )  e.  { t  e. 
U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  <->  ( ( 1st `  y
)  e.  U. R  /\  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  x
) )
6356, 59, 62sylanbrc 645 . . . . . . . 8  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  ( 1st `  y )  e. 
{ t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }
)
64 nlly2i 17202 . . . . . . . 8  |-  ( ( R  e. 𝑛Locally  Comp  /\  { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  e.  R  /\  ( 1st `  y )  e. 
{ t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }
)  ->  E. s  e.  ~P  { t  e. 
U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x } E. u  e.  R  ( ( 1st `  y
)  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) )
658, 54, 63, 64syl3anc 1182 . . . . . . 7  |-  ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  ->  E. s  e.  ~P  { t  e. 
U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x } E. u  e.  R  ( ( 1st `  y
)  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) )
6611adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  R  e.  Top )
6718adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  S  e.  Top )
68 simprlr 739 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  u  e.  R
)
69 ssrab2 3258 . . . . . . . . . . . . . 14  |-  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  C_  U. S
7069a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x }  C_  U. S )
71 incom 3361 . . . . . . . . . . . . . . . 16  |-  ( { v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x }  i^i  k )  =  ( k  i^i  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x } )
72 simprll 738 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }
)
73 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x }  ->  s  C_  { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x } )
7472, 73syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  s  C_  { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x } )
75 ssrab2 3258 . . . . . . . . . . . . . . . . . . . . . 22  |-  { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x }  C_  U. R
7674, 75syl6ss 3191 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  s  C_  U. R
)
7776adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  s  C_ 
U. R )
78 elpwi 3633 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ~P U. S  ->  k  C_  U. S )
7978ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  k  C_ 
U. S )
80 eldif 3162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  ( ( s  X.  k )  \  x )  <->  ( t  e.  ( s  X.  k
)  /\  -.  t  e.  x ) )
8180anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( t  e.  ( ( s  X.  k ) 
\  x )  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b )  <-> 
( ( t  e.  ( s  X.  k
)  /\  -.  t  e.  x )  /\  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b ) )
82 anass 630 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( t  e.  ( s  X.  k )  /\  -.  t  e.  x )  /\  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b )  <->  ( t  e.  ( s  X.  k
)  /\  ( -.  t  e.  x  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b ) ) )
8381, 82bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( t  e.  ( ( s  X.  k ) 
\  x )  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b )  <-> 
( t  e.  ( s  X.  k )  /\  ( -.  t  e.  x  /\  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b ) ) )
8483rexbii2 2572 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. t  e.  ( ( s  X.  k ) 
\  x ) ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b  <->  E. t  e.  ( s  X.  k
) ( -.  t  e.  x  /\  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b ) )
85 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  t  e.  x  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b )  <-> 
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b  /\  -.  t  e.  x ) )
86 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  <. a ,  u >.  ->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  <. a ,  u >. )
)
8786eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  <. a ,  u >.  ->  ( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b  <->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) `
 <. a ,  u >. )  =  b ) )
88 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  <. a ,  u >.  ->  ( t  e.  x  <->  <. a ,  u >.  e.  x ) )
8988notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  <. a ,  u >.  ->  ( -.  t  e.  x  <->  -.  <. a ,  u >.  e.  x
) )
9087, 89anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  <. a ,  u >.  ->  ( ( ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b  /\  -.  t  e.  x
)  <->  ( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <. a ,  u >.  e.  x
) ) )
9185, 90syl5bb 248 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  <. a ,  u >.  ->  ( ( -.  t  e.  x  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b )  <-> 
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <.
a ,  u >.  e.  x ) ) )
9291rexxp 4828 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. t  e.  ( s  X.  k ) ( -.  t  e.  x  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b )  <->  E. a  e.  s  E. u  e.  k 
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <.
a ,  u >.  e.  x ) )
9384, 92bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. t  e.  ( ( s  X.  k ) 
\  x ) ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b  <->  E. a  e.  s  E. u  e.  k  ( (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <. a ,  u >.  e.  x
) )
94 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  s  C_  U. R
)
9594sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  a  e.  U. R )
9695adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  a  e.  U. R )
97 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  k  C_ 
U. S )
9897sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  u  e.  U. S )
99 opelxpi 4721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( a  e.  U. R  /\  u  e.  U. S
)  ->  <. a ,  u >.  e.  ( U. R  X.  U. S
) )
10096, 98, 99syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  <. a ,  u >.  e.  ( U. R  X.  U. S
) )
101 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
a ,  u >.  e.  ( U. R  X.  U. S )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  ( 2nd `  <. a ,  u >. ) )
102100, 101syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  ( 2nd `  <. a ,  u >. ) )
103 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  a  e. 
_V
104 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  u  e. 
_V
105103, 104op2nd 6129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2nd `  <. a ,  u >. )  =  u
106102, 105syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  u )
107106eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  (
( ( 2nd  |`  ( U. R  X.  U. S
) ) `  <. a ,  u >. )  =  b  <->  u  =  b
) )
108107anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  (
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <.
a ,  u >.  e.  x )  <->  ( u  =  b  /\  -.  <. a ,  u >.  e.  x
) ) )
109108rexbidva 2560 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  ( E. u  e.  k 
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <.
a ,  u >.  e.  x )  <->  E. u  e.  k  ( u  =  b  /\  -.  <. a ,  u >.  e.  x
) ) )
110 opeq2 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  b  ->  <. a ,  u >.  =  <. a ,  b >. )
111110eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  =  b  ->  ( <. a ,  u >.  e.  x  <->  <. a ,  b
>.  e.  x ) )
112111notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  =  b  ->  ( -.  <. a ,  u >.  e.  x  <->  -.  <. a ,  b >.  e.  x
) )
113112ceqsrexbv 2902 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. u  e.  k  ( u  =  b  /\  -.  <. a ,  u >.  e.  x )  <->  ( b  e.  k  /\  -.  <. a ,  b >.  e.  x
) )
114109, 113syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  ( E. u  e.  k 
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <.
a ,  u >.  e.  x )  <->  ( b  e.  k  /\  -.  <. a ,  b >.  e.  x
) ) )
115114rexbidva 2560 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( E. a  e.  s  E. u  e.  k  ( (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <. a ,  u >.  e.  x
)  <->  E. a  e.  s  ( b  e.  k  /\  -.  <. a ,  b >.  e.  x
) ) )
116 r19.42v 2694 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. a  e.  s  ( b  e.  k  /\  -.  <. a ,  b
>.  e.  x )  <->  ( b  e.  k  /\  E. a  e.  s  -.  <. a ,  b >.  e.  x
) )
117115, 116syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( E. a  e.  s  E. u  e.  k  ( (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  b  /\  -.  <. a ,  u >.  e.  x
)  <->  ( b  e.  k  /\  E. a  e.  s  -.  <. a ,  b >.  e.  x
) ) )
11893, 117syl5bb 248 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( E. t  e.  ( ( s  X.  k )  \  x
) ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b  <-> 
( b  e.  k  /\  E. a  e.  s  -.  <. a ,  b >.  e.  x
) ) )
119 f2ndres 6142 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd  |`  ( U. R  X.  U. S ) ) : ( U. R  X.  U. S ) --> U. S
120 ffn 5389 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) : ( U. R  X.  U. S ) --> U. S  ->  ( 2nd  |`  ( U. R  X.  U. S ) )  Fn  ( U. R  X.  U. S ) )
121119, 120ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2nd  |`  ( U. R  X.  U. S ) )  Fn  ( U. R  X.  U. S )
122 difss 3303 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  X.  k ) 
\  x )  C_  ( s  X.  k
)
123 xpss12 4792 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( s  X.  k )  C_  ( U. R  X.  U. S
) )
124122, 123syl5ss 3190 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( ( s  X.  k )  \  x )  C_  ( U. R  X.  U. S
) )
125 fvelimab 5578 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 2nd  |`  ( U. R  X.  U. S
) )  Fn  ( U. R  X.  U. S
)  /\  ( (
s  X.  k ) 
\  x )  C_  ( U. R  X.  U. S ) )  -> 
( b  e.  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
)  <->  E. t  e.  ( ( s  X.  k
)  \  x )
( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b ) )
126121, 124, 125sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( b  e.  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
)  <->  E. t  e.  ( ( s  X.  k
)  \  x )
( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b ) )
127 eldif 3162 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  ( k  \  { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } )  <-> 
( b  e.  k  /\  -.  b  e. 
{ v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) )
128 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  k  C_  U. S
)
129128sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  b  e.  k )  ->  b  e.  U. S )
130 sneq 3651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  =  b  ->  { v }  =  { b } )
131130xpeq2d 4713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( v  =  b  ->  (
s  X.  { v } )  =  ( s  X.  { b } ) )
132131sseq1d 3205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( v  =  b  ->  (
( s  X.  {
v } )  C_  x 
<->  ( s  X.  {
b } )  C_  x ) )
133 dfss3 3170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( s  X.  { b } )  C_  x  <->  A. k  e.  ( s  X.  { b } ) k  e.  x
)
134 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  <. a ,  t
>.  ->  ( k  e.  x  <->  <. a ,  t
>.  e.  x ) )
135134ralxp 4827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. k  e.  ( s  X.  { b } ) k  e.  x  <->  A. a  e.  s  A. t  e.  { b } <. a ,  t >.  e.  x
)
136 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  b  e. 
_V
137 opeq2 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  b  ->  <. a ,  t >.  =  <. a ,  b >. )
138137eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  b  ->  ( <. a ,  t >.  e.  x  <->  <. a ,  b
>.  e.  x ) )
139136, 138ralsn 3674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. t  e.  { b } <. a ,  t
>.  e.  x  <->  <. a ,  b >.  e.  x
)
140139ralbii 2567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. a  e.  s  A. t  e.  { b } <. a ,  t
>.  e.  x  <->  A. a  e.  s  <. a ,  b >.  e.  x
)
141133, 135, 1403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  X.  { b } )  C_  x  <->  A. a  e.  s  <. a ,  b >.  e.  x
)
142132, 141syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( v  =  b  ->  (
( s  X.  {
v } )  C_  x 
<-> 
A. a  e.  s 
<. a ,  b >.  e.  x ) )
143142elrab3 2924 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  e.  U. S  -> 
( b  e.  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x }  <->  A. a  e.  s  <. a ,  b >.  e.  x
) )
144129, 143syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  b  e.  k )  ->  (
b  e.  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  <->  A. a  e.  s 
<. a ,  b >.  e.  x ) )
145144notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  b  e.  k )  ->  ( -.  b  e.  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  <->  -.  A. a  e.  s  <. a ,  b >.  e.  x
) )
146 rexnal 2554 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. a  e.  s  -. 
<. a ,  b >.  e.  x  <->  -.  A. a  e.  s  <. a ,  b >.  e.  x
)
147145, 146syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  b  e.  k )  ->  ( -.  b  e.  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  <->  E. a  e.  s  -.  <. a ,  b
>.  e.  x ) )
148147pm5.32da 622 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( ( b  e.  k  /\  -.  b  e.  { v  e.  U. S  |  ( s  X.  { v } )  C_  x } )  <->  ( b  e.  k  /\  E. a  e.  s  -.  <. a ,  b >.  e.  x
) ) )
149127, 148syl5bb 248 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( b  e.  ( k  \  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x } )  <-> 
( b  e.  k  /\  E. a  e.  s  -.  <. a ,  b >.  e.  x
) ) )
150118, 126, 1493bitr4d 276 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( b  e.  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
)  <->  b  e.  ( k  \  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x } ) ) )
151150eqrdv 2281 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) "
( ( s  X.  k )  \  x
) )  =  ( k  \  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x } ) )
15277, 79, 151syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  =  ( k  \  { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) )
153 difin 3406 . . . . . . . . . . . . . . . . . . . 20  |-  ( k 
\  ( k  i^i 
{ v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) )  =  ( k 
\  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x } )
15467adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  S  e.  Top )
15519restuni 16893 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  Top  /\  k  C_  U. S )  ->  k  =  U. ( St  k ) )
156154, 79, 155syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  k  =  U. ( St  k ) )
157156difeq1d 3293 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
k  \  ( k  i^i  { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) )  =  ( U. ( St  k )  \ 
( k  i^i  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x } ) ) )
158153, 157syl5eqr 2329 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
k  \  { v  e.  U. S  |  ( s  X.  { v } )  C_  x } )  =  ( U. ( St  k ) 
\  ( k  i^i 
{ v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) ) )
159152, 158eqtrd 2315 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  =  ( U. ( St  k )  \  (
k  i^i  { v  e.  U. S  |  ( s  X.  { v } )  C_  x } ) ) )
160 inss2 3390 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 𝑘Gen  i^i 
Haus )  C_  Haus
16117ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  S  e.  ( ran 𝑘Gen  i^i  Haus )
)
162160, 161sseldi 3178 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  S  e.  Haus )
163 df-ima 4702 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  =  ran  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) )
164 resres 4968 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) )  =  ( 2nd  |`  (
( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
) )
165 inss2 3390 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( (
s  X.  k ) 
\  x )
166165, 122sstri 3188 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( s  X.  k )
167 ssres2 4982 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( s  X.  k )  ->  ( 2nd  |`  ( ( U. R  X.  U. S )  i^i  ( ( s  X.  k )  \  x ) ) ) 
C_  ( 2nd  |`  (
s  X.  k ) ) )
168166, 167ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd  |`  ( ( U. R  X.  U. S )  i^i  ( ( s  X.  k )  \  x
) ) )  C_  ( 2nd  |`  ( s  X.  k ) )
169164, 168eqsstri 3208 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) ) 
C_  ( 2nd  |`  (
s  X.  k ) )
170 rnss 4907 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2nd  |`  ( U. R  X.  U. S
) )  |`  (
( s  X.  k
)  \  x )
)  C_  ( 2nd  |`  ( s  X.  k
) )  ->  ran  ( ( 2nd  |`  ( U. R  X.  U. S
) )  |`  (
( s  X.  k
)  \  x )
)  C_  ran  ( 2nd  |`  ( s  X.  k
) ) )
171169, 170ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  (
( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) ) 
C_  ran  ( 2nd  |`  ( s  X.  k
) )
172163, 171eqsstri 3208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  ran  ( 2nd  |`  ( s  X.  k
) )
173 f2ndres 6142 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2nd  |`  ( s  X.  k
) ) : ( s  X.  k ) --> k
174 frn 5395 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2nd  |`  ( s  X.  k ) ) : ( s  X.  k
) --> k  ->  ran  ( 2nd  |`  ( s  X.  k ) )  C_  k )
175173, 174ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ran  ( 2nd  |`  ( s  X.  k ) )  C_  k
176172, 175sstri 3188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  k
177176, 79syl5ss 3190 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  U. S )
17814ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  R  e.  (TopOn `  U. R ) )
179154, 20sylib 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  S  e.  (TopOn `  U. S ) )
180 tx2cn 17304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  (TopOn `  U. R )  /\  S  e.  (TopOn `  U. S ) )  ->  ( 2nd  |`  ( U. R  X.  U. S ) )  e.  ( ( R  tX  S )  Cn  S
) )
181178, 179, 180syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( 2nd  |`  ( U. R  X.  U. S ) )  e.  ( ( R 
tX  S )  Cn  S ) )
18228ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( R  tX  S )  e. 
Top )
183122a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( s  X.  k
)  \  x )  C_  ( s  X.  k
) )
184 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
185 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  k  e. 
_V
186184, 185xpex 4801 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  X.  k )  e. 
_V
187186a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
s  X.  k )  e.  _V )
188 restabs 16896 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( R  tX  S
)  e.  Top  /\  ( ( s  X.  k )  \  x
)  C_  ( s  X.  k )  /\  (
s  X.  k )  e.  _V )  -> 
( ( ( R 
tX  S )t  ( s  X.  k ) )t  ( ( s  X.  k
)  \  x )
)  =  ( ( R  tX  S )t  ( ( s  X.  k
)  \  x )
) )
189182, 183, 187, 188syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( ( R  tX  S )t  ( s  X.  k ) )t  ( ( s  X.  k ) 
\  x ) )  =  ( ( R 
tX  S )t  ( ( s  X.  k ) 
\  x ) ) )
19066adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  R  e.  Top )
191161, 5syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  S  e.  Top )
192184a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  s  e.  _V )
193 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  k  e.  ~P U. S )
194 txrest 17325 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( R  e.  Top  /\  S  e.  Top )  /\  ( s  e.  _V  /\  k  e.  ~P U. S ) )  -> 
( ( R  tX  S )t  ( s  X.  k ) )  =  ( ( Rt  s ) 
tX  ( St  k ) ) )
195190, 191, 192, 193, 194syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( R  tX  S
)t  ( s  X.  k
) )  =  ( ( Rt  s )  tX  ( St  k ) ) )
196 simprr3 1005 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  ( Rt  s )  e.  Comp )
197196adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( Rt  s )  e.  Comp )
198 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( St  k )  e.  Comp )
199 txcmp 17337 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Rt  s )  e. 
Comp  /\  ( St  k )  e.  Comp )  ->  (
( Rt  s )  tX  ( St  k ) )  e.  Comp )
200197, 198, 199syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( Rt  s )  tX  ( St  k ) )  e.  Comp )
201195, 200eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( R  tX  S
)t  ( s  X.  k
) )  e.  Comp )
202 difin 3406 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  X.  k ) 
\  ( ( s  X.  k )  i^i  x ) )  =  ( ( s  X.  k )  \  x
)
20377, 79, 123syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
s  X.  k ) 
C_  ( U. R  X.  U. S ) )
204190, 154, 26syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( U. R  X.  U. S
)  =  U. ( R  tX  S ) )
205203, 204sseqtrd 3214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
s  X.  k ) 
C_  U. ( R  tX  S ) )
20629restuni 16893 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( R  tX  S
)  e.  Top  /\  ( s  X.  k
)  C_  U. ( R  tX  S ) )  ->  ( s  X.  k )  =  U. ( ( R  tX  S )t  ( s  X.  k ) ) )
207182, 205, 206syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
s  X.  k )  =  U. ( ( R  tX  S )t  ( s  X.  k ) ) )
208207difeq1d 3293 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( s  X.  k
)  \  ( (
s  X.  k )  i^i  x ) )  =  ( U. (
( R  tX  S
)t  ( s  X.  k
) )  \  (
( s  X.  k
)  i^i  x )
) )
209202, 208syl5eqr 2329 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( s  X.  k
)  \  x )  =  ( U. (
( R  tX  S
)t  ( s  X.  k
) )  \  (
( s  X.  k
)  i^i  x )
) )
210 resttop 16891 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( R  tX  S
)  e.  Top  /\  ( s  X.  k
)  e.  _V )  ->  ( ( R  tX  S )t  ( s  X.  k ) )  e. 
Top )
211182, 186, 210sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( R  tX  S
)t  ( s  X.  k
) )  e.  Top )
212 incom 3361 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  X.  k )  i^i  x )  =  ( x  i^i  (
s  X.  k ) )
21323ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  x  e.  (𝑘Gen `  ( R  tX  S ) ) )
214 kgeni 17232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  (𝑘Gen `  ( R  tX  S ) )  /\  ( ( R 
tX  S )t  ( s  X.  k ) )  e.  Comp )  ->  (
x  i^i  ( s  X.  k ) )  e.  ( ( R  tX  S )t  ( s  X.  k ) ) )
215213, 201, 214syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
x  i^i  ( s  X.  k ) )  e.  ( ( R  tX  S )t  ( s  X.  k ) ) )
216212, 215syl5eqel 2367 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( s  X.  k
)  i^i  x )  e.  ( ( R  tX  S )t  ( s  X.  k ) ) )
217 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. (
( R  tX  S
)t  ( s  X.  k
) )  =  U. ( ( R  tX  S )t  ( s  X.  k ) )
218217opncld 16770 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( R  tX  S )t  ( s  X.  k ) )  e. 
Top  /\  ( (
s  X.  k )  i^i  x )  e.  ( ( R  tX  S )t  ( s  X.  k ) ) )  ->  ( U. (
( R  tX  S
)t  ( s  X.  k
) )  \  (
( s  X.  k
)  i^i  x )
)  e.  ( Clsd `  ( ( R  tX  S )t  ( s  X.  k ) ) ) )
219211, 216, 218syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( U. ( ( R  tX  S )t  ( s  X.  k ) )  \ 
( ( s  X.  k )  i^i  x
) )  e.  (
Clsd `  ( ( R  tX  S )t  ( s  X.  k ) ) ) )
220209, 219eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( s  X.  k
)  \  x )  e.  ( Clsd `  (
( R  tX  S
)t  ( s  X.  k
) ) ) )
221 cmpcld 17129 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( R  tX  S )t  ( s  X.  k ) )  e. 
Comp  /\  ( ( s  X.  k )  \  x )  e.  (
Clsd `  ( ( R  tX  S )t  ( s  X.  k ) ) ) )  ->  (
( ( R  tX  S )t  ( s  X.  k ) )t  ( ( s  X.  k ) 
\  x ) )  e.  Comp )
222201, 220, 221syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( ( R  tX  S )t  ( s  X.  k ) )t  ( ( s  X.  k ) 
\  x ) )  e.  Comp )
223189, 222eqeltrrd 2358 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( R  tX  S
)t  ( ( s  X.  k )  \  x
) )  e.  Comp )
224 imacmp 17124 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 2nd  |`  ( U. R  X.  U. S
) )  e.  ( ( R  tX  S
)  Cn  S )  /\  ( ( R 
tX  S )t  ( ( s  X.  k ) 
\  x ) )  e.  Comp )  ->  ( St  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
) )  e.  Comp )
225181, 223, 224syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( St  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
) )  e.  Comp )
22619hauscmp 17134 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( S  e.  Haus  /\  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  U. S  /\  ( St  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
) )  e.  Comp )  ->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) "
( ( s  X.  k )  \  x
) )  e.  (
Clsd `  S )
)
227162, 177, 225, 226syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  e.  ( Clsd `  S
) )
228176a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  k )
22919restcldi 16904 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  C_  U. S  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
)  e.  ( Clsd `  S )  /\  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  k )  -> 
( ( 2nd  |`  ( U. R  X.  U. S
) ) " (
( s  X.  k
)  \  x )
)  e.  ( Clsd `  ( St  k ) ) )
23079, 227, 228, 229syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  e.  ( Clsd `  ( St  k ) ) )
231159, 230eqeltrrd 2358 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( U. ( St  k )  \ 
( k  i^i  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x } ) )  e.  ( Clsd `  ( St  k ) ) )
232 resttop 16891 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  e.  Top  /\  k  e.  ~P U. S
)  ->  ( St  k
)  e.  Top )
233154, 193, 232syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( St  k )  e.  Top )
234 inss1 3389 . . . . . . . . . . . . . . . . . . 19  |-  ( k  i^i  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x } )  C_  k
235234, 156syl5sseq 3226 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
k  i^i  { v  e.  U. S  |  ( s  X.  { v } )  C_  x } )  C_  U. ( St  k ) )
236 eqid 2283 . . . . . . . . . . . . . . . . . . 19  |-  U. ( St  k )  =  U. ( St  k )
237236isopn2 16769 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( St  k )  e. 
Top  /\  ( k  i^i  { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) 
C_  U. ( St  k ) )  ->  ( (
k  i^i  { v  e.  U. S  |  ( s  X.  { v } )  C_  x } )  e.  ( St  k )  <->  ( U. ( St  k )  \ 
( k  i^i  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x } ) )  e.  ( Clsd `  ( St  k ) ) ) )
238233, 235, 237syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
( k  i^i  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x } )  e.  ( St  k )  <-> 
( U. ( St  k )  \  ( k  i^i  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x } ) )  e.  ( Clsd `  ( St  k ) ) ) )
239231, 238mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  (
k  i^i  { v  e.  U. S  |  ( s  X.  { v } )  C_  x } )  e.  ( St  k ) )
24071, 239syl5eqel 2367 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  ( k  e. 
~P U. S  /\  ( St  k )  e.  Comp ) )  ->  ( { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x }  i^i  k )  e.  ( St  k ) )
241240expr 598 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  /\  k  e.  ~P U. S )  ->  (
( St  k )  e. 
Comp  ->  ( { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  i^i  k
)  e.  ( St  k ) ) )
242241ralrimiva 2626 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  A. k  e.  ~P  U. S ( ( St  k )  e.  Comp  ->  ( { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x }  i^i  k )  e.  ( St  k ) ) )
24367, 20sylib 188 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  S  e.  (TopOn `  U. S ) )
244 elkgen 17231 . . . . . . . . . . . . . 14  |-  ( S  e.  (TopOn `  U. S )  ->  ( { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x }  e.  (𝑘Gen
`  S )  <->  ( {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x }  C_  U. S  /\  A. k  e.  ~P  U. S ( ( St  k )  e. 
Comp  ->  ( { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  i^i  k
)  e.  ( St  k ) ) ) ) )
245243, 244syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  ( { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  e.  (𝑘Gen `  S )  <->  ( {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x }  C_  U. S  /\  A. k  e.  ~P  U. S ( ( St  k )  e. 
Comp  ->  ( { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  i^i  k
)  e.  ( St  k ) ) ) ) )
24670, 242, 245mpbir2and 888 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x }  e.  (𝑘Gen `  S
) )
24717adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  S  e.  ( ran 𝑘Gen  i^i  Haus ) )
248247, 3syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  S  e.  ran 𝑘Gen )
249 kgenidm 17242 . . . . . . . . . . . . 13  |-  ( S  e.  ran 𝑘Gen  ->  (𝑘Gen `  S
)  =  S )
250248, 249syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  (𝑘Gen `  S )  =  S )
251246, 250eleqtrd 2359 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x }  e.  S )
252 txopn 17297 . . . . . . . . . . 11  |-  ( ( ( R  e.  Top  /\  S  e.  Top )  /\  ( u  e.  R  /\  { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x }  e.  S ) )  -> 
( u  X.  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x } )  e.  ( R  tX  S ) )
25366, 67, 68, 251, 252syl22anc 1183 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  ( u  X.  { v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } )  e.  ( R  tX  S ) )
25458adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
255 simprr1 1003 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  ( 1st `  y
)  e.  u )
25635adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e. 𝑛Locally 
Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  /\  y  e.  x )  /\  (
( s  e.  ~P { t  e.  U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }  /\  u  e.  R
)  /\  ( ( 1st `  y )  e.  u  /\  u  C_  s  /\  ( Rt  s )  e.  Comp ) ) )  ->  ( 2nd `  y
)