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

Theorem txkgen 20443
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.)
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 20264 . . 3  |-  ( R  e. 𝑛Locally 
Comp  ->  R  e.  Top )
2 inss1 3658 . . . . 5  |-  ( ran 𝑘Gen  i^i 
Haus )  C_  ran 𝑘Gen
32sseli 3437 . . . 4  |-  ( S  e.  ( ran 𝑘Gen  i^i  Haus )  ->  S  e.  ran 𝑘Gen )
4 kgentop 20333 . . . 4  |-  ( S  e.  ran 𝑘Gen  ->  S  e.  Top )
53, 4syl 17 . . 3  |-  ( S  e.  ( ran 𝑘Gen  i^i  Haus )  ->  S  e.  Top )
6 txtop 20360 . . 3  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( R  tX  S
)  e.  Top )
71, 5, 6syl2an 475 . 2  |-  ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  -> 
( R  tX  S
)  e.  Top )
8 simplll 760 . . . . . . . 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 2402 . . . . . . . . . 10  |-  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )  =  ( t  e. 
U. R  |->  <. t ,  ( 2nd `  y
) >. )
109mptpreima 5315 . . . . . . . . 9  |-  ( `' ( t  e.  U. R  |->  <. t ,  ( 2nd `  y )
>. ) " x )  =  { t  e. 
U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }
111ad3antrrr 728 . . . . . . . . . . . . . 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 2402 . . . . . . . . . . . . . . 15  |-  U. R  =  U. R
1312toptopon 19724 . . . . . . . . . . . . . 14  |-  ( R  e.  Top  <->  R  e.  (TopOn `  U. R ) )
1411, 13sylib 196 . . . . . . . . . . . . 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 20049 . . . . . . . . . . . . 13  |-  ( R  e.  (TopOn `  U. R )  ->  (  _I  |`  U. R )  e.  ( R  Cn  R ) )
1614, 15syl 17 . . . . . . . . . . . 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 761 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 2402 . . . . . . . . . . . . . . 15  |-  U. S  =  U. S
2019toptopon 19724 . . . . . . . . . . . . . 14  |-  ( S  e.  Top  <->  S  e.  (TopOn `  U. S ) )
2118, 20sylib 196 . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . 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 4195 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  x  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  ->  y  e.  U. (𝑘Gen `  ( R  tX  S ) ) )
2522, 23, 24syl2anc 659 . . . . . . . . . . . . . . 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 20383 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( U. R  X.  U. S )  =  U. ( R  tX  S ) )
2711, 18, 26syl2anc 659 . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . 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 2402 . . . . . . . . . . . . . . . . . 18  |-  U. ( R  tX  S )  = 
U. ( R  tX  S )
3029kgenuni 20330 . . . . . . . . . . . . . . . . 17  |-  ( ( R  tX  S )  e.  Top  ->  U. ( R  tX  S )  = 
U. (𝑘Gen `  ( R  tX  S ) ) )
3128, 30syl 17 . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 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 2493 . . . . . . . . . . . . . 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 6814 . . . . . . . . . . . . . 14  |-  ( y  e.  ( U. R  X.  U. S )  -> 
( 2nd `  y
)  e.  U. S
)
3533, 34syl 17 . . . . . . . . . . . . 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 20075 . . . . . . . . . . . . 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 1230 . . . . . . . . . . . 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 6076 . . . . . . . . . . . . . . . 16  |-  ( t  e.  U. R  -> 
( (  _I  |`  U. R
) `  t )  =  t )
39 fvex 5858 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  y )  e.  _V
4039fvconst2 6106 . . . . . . . . . . . . . . . 16  |-  ( t  e.  U. R  -> 
( ( U. R  X.  { ( 2nd `  y
) } ) `  t )  =  ( 2nd `  y ) )
4138, 40opeq12d 4166 . . . . . . . . . . . . . . 15  |-  ( t  e.  U. R  ->  <. ( (  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.  =  <. t ,  ( 2nd `  y )
>. )
4241mpteq2ia 4476 . . . . . . . . . . . . . 14  |-  ( t  e.  U. R  |->  <.
( (  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.
)  =  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )
4342eqcomi 2415 . . . . . . . . . . . . 13  |-  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )  =  ( t  e. 
U. R  |->  <. (
(  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.
)
4412, 43txcnmpt 20415 . . . . . . . . . . . 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 659 . . . . . . . . . . 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 20343 . . . . . . . . . . . . 13  |-  ( R  e. 𝑛Locally 
Comp  ->  R  e.  ran 𝑘Gen )
4746ad3antrrr 728 . . . . . . . . . . . 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 724 . . . . . . . . . . . 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 20349 . . . . . . . . . . . 12  |-  ( ( R  e.  ran 𝑘Gen  /\  ( R  tX  S )  e. 
Top )  ->  ( R  Cn  ( R  tX  S ) )  =  ( R  Cn  (𝑘Gen `  ( R  tX  S ) ) ) )
5047, 48, 49syl2anc 659 . . . . . . . . . . 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 2492 . . . . . . . . . 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 20057 . . . . . . . . . 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 659 . . . . . . . . 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 2495 . . . . . . . 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 6813 . . . . . . . . . 10  |-  ( y  e.  ( U. R  X.  U. S )  -> 
( 1st `  y
)  e.  U. R
)
5633, 55syl 17 . . . . . . . . 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 6820 . . . . . . . . . . 11  |-  ( y  e.  ( U. R  X.  U. S )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
5833, 57syl 17 . . . . . . . . . 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 2491 . . . . . . . . 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 4158 . . . . . . . . . . 11  |-  ( t  =  ( 1st `  y
)  ->  <. t ,  ( 2nd `  y
) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
6160eleq1d 2471 . . . . . . . . . 10  |-  ( t  =  ( 1st `  y
)  ->  ( <. t ,  ( 2nd `  y
) >.  e.  x  <->  <. ( 1st `  y ) ,  ( 2nd `  y )
>.  e.  x ) )
6261elrab 3206 . . . . . . . . 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 662 . . . . . . . 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 20267 . . . . . . . 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 1230 . . . . . . 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 463 . . . . . . . . . . 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 463 . . . . . . . . . . 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 765 . . . . . . . . . . 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 3523 . . . . . . . . . . . . . 14  |-  { v  e.  U. S  | 
( s  X.  {
v } )  C_  x }  C_  U. S
7069a1i 11 . . . . . . . . . . . . 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 3631 . . . . . . . . . . . . . . . 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 764 . . . . . . . . . . . . . . . . . . . . . . 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 }
)
7372elpwid 3964 . . . . . . . . . . . . . . . . . . . . . 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 } )
74 ssrab2 3523 . . . . . . . . . . . . . . . . . . . . . 22  |-  { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x }  C_  U. R
7573, 74syl6ss 3453 . . . . . . . . . . . . . . . . . . . . 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
)
7675adantr 463 . . . . . . . . . . . . . . . . . . . 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 )
77 elpwi 3963 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ~P U. S  ->  k  C_  U. S )
7877ad2antrl 726 . . . . . . . . . . . . . . . . . . . 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 )
79 eldif 3423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  ( ( s  X.  k )  \  x )  <->  ( t  e.  ( s  X.  k
)  /\  -.  t  e.  x ) )
8079anbi1i 693 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
81 anass 647 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
8280, 81bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
8382rexbii2 2903 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
84 ancom 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  t  e.  x  /\  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  t
)  =  b )  <-> 
( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b  /\  -.  t  e.  x ) )
85 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  <. a ,  u >.  ->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  <. a ,  u >. )
)
8685eqeq1d 2404 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  <. a ,  u >.  ->  ( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b  <->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) `
 <. a ,  u >. )  =  b ) )
87 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  <. a ,  u >.  ->  ( t  e.  x  <->  <. a ,  u >.  e.  x ) )
8887notbid 292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  <. a ,  u >.  ->  ( -.  t  e.  x  <->  -.  <. a ,  u >.  e.  x
) )
8986, 88anbi12d 709 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
9084, 89syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
9190rexxp 4965 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
9283, 91bitri 249 . . . . . . . . . . . . . . . . . . . . . . 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
) )
93 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  s  C_  U. R
)
9493sselda 3441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  a  e.  U. R )
9594adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  a  e.  U. R )
96 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  k  C_ 
U. S )
9796sselda 3441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  u  e.  U. S )
98 opelxpi 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( a  e.  U. R  /\  u  e.  U. S
)  ->  <. a ,  u >.  e.  ( U. R  X.  U. S
) )
9995, 97, 98syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  <. a ,  u >.  e.  ( U. R  X.  U. S
) )
100 fvres 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
a ,  u >.  e.  ( U. R  X.  U. S )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  ( 2nd `  <. a ,  u >. ) )
10199, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 >. ) )
102 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  a  e. 
_V
103 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  u  e. 
_V
104102, 103op2nd 6792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2nd `  <. a ,  u >. )  =  u
105101, 104syl6eq 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  u )
106105eqeq1d 2404 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
107106anbi1d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
108107rexbidva 2914 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
109 opeq2 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  b  ->  <. a ,  u >.  =  <. a ,  b >. )
110109eleq1d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  =  b  ->  ( <. a ,  u >.  e.  x  <->  <. a ,  b
>.  e.  x ) )
111110notbid 292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  =  b  ->  ( -.  <. a ,  u >.  e.  x  <->  -.  <. a ,  b >.  e.  x
) )
112111ceqsrexbv 3183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. u  e.  k  ( u  =  b  /\  -.  <. a ,  u >.  e.  x )  <->  ( b  e.  k  /\  -.  <. a ,  b >.  e.  x
) )
113108, 112syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
114113rexbidva 2914 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
115 r19.42v 2961 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. a  e.  s  ( b  e.  k  /\  -.  <. a ,  b
>.  e.  x )  <->  ( b  e.  k  /\  E. a  e.  s  -.  <. a ,  b >.  e.  x
) )
116114, 115syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
11792, 116syl5bb 257 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
118 f2ndres 6806 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd  |`  ( U. R  X.  U. S ) ) : ( U. R  X.  U. S ) --> U. S
119 ffn 5713 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
120118, 119ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2nd  |`  ( U. R  X.  U. S ) )  Fn  ( U. R  X.  U. S )
121 difss 3569 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  X.  k ) 
\  x )  C_  ( s  X.  k
)
122 xpss12 4928 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( s  X.  k )  C_  ( U. R  X.  U. S
) )
123121, 122syl5ss 3452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( ( s  X.  k )  \  x )  C_  ( U. R  X.  U. S
) )
124 fvelimab 5904 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
125120, 123, 124sylancr 661 . . . . . . . . . . . . . . . . . . . . . 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 ) )
126 eldif 3423 . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
127 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  k  C_  U. S
)
128127sselda 3441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  b  e.  k )  ->  b  e.  U. S )
129 sneq 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  =  b  ->  { v }  =  { b } )
130129xpeq2d 4846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( v  =  b  ->  (
s  X.  { v } )  =  ( s  X.  { b } ) )
131130sseq1d 3468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( v  =  b  ->  (
( s  X.  {
v } )  C_  x 
<->  ( s  X.  {
b } )  C_  x ) )
132 dfss3 3431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( s  X.  { b } )  C_  x  <->  A. k  e.  ( s  X.  { b } ) k  e.  x
)
133 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  <. a ,  t
>.  ->  ( k  e.  x  <->  <. a ,  t
>.  e.  x ) )
134133ralxp 4964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. k  e.  ( s  X.  { b } ) k  e.  x  <->  A. a  e.  s  A. t  e.  { b } <. a ,  t >.  e.  x
)
135 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  b  e. 
_V
136 opeq2 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  b  ->  <. a ,  t >.  =  <. a ,  b >. )
137136eleq1d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  b  ->  ( <. a ,  t >.  e.  x  <->  <. a ,  b
>.  e.  x ) )
138135, 137ralsn 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. t  e.  { b } <. a ,  t
>.  e.  x  <->  <. a ,  b >.  e.  x
)
139138ralbii 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. a  e.  s  A. t  e.  { b } <. a ,  t
>.  e.  x  <->  A. a  e.  s  <. a ,  b >.  e.  x
)
140132, 134, 1393bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  X.  { b } )  C_  x  <->  A. a  e.  s  <. a ,  b >.  e.  x
)
141131, 140syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( v  =  b  ->  (
( s  X.  {
v } )  C_  x 
<-> 
A. a  e.  s 
<. a ,  b >.  e.  x ) )
142141elrab3 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  e.  U. S  -> 
( b  e.  {
v  e.  U. S  |  ( s  X. 
{ v } ) 
C_  x }  <->  A. a  e.  s  <. a ,  b >.  e.  x
) )
143128, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
144143notbid 292 . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
145 rexnal 2851 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. a  e.  s  -. 
<. a ,  b >.  e.  x  <->  -.  A. a  e.  s  <. a ,  b >.  e.  x
)
146144, 145syl6bbr 263 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
147146pm5.32da 639 . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
148126, 147syl5bb 257 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
149117, 125, 1483bitr4d 285 . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
150149eqrdv 2399 . . . . . . . . . . . . . . . . . . . 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 } ) )
15176, 78, 150syl2anc 659 . . . . . . . . . . . . . . . . . . 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 } ) )
152 difin 3686 . . . . . . . . . . . . . . . . . . . 20  |-  ( k 
\  ( k  i^i 
{ v  e.  U. S  |  ( s  X.  { v } ) 
C_  x } ) )  =  ( k 
\  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x } )
15367adantr 463 . . . . . . . . . . . . . . . . . . . . . 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 )
15419restuni 19954 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  Top  /\  k  C_  U. S )  ->  k  =  U. ( St  k ) )
155153, 78, 154syl2anc 659 . . . . . . . . . . . . . . . . . . . . 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 ) )
156155difeq1d 3559 . . . . . . . . . . . . . . . . . . . 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 } ) ) )
157152, 156syl5eqr 2457 . . . . . . . . . . . . . . . . . . 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 } ) ) )
158151, 157eqtrd 2443 . . . . . . . . . . . . . . . . . 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 } ) ) )
159 inss2 3659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 𝑘Gen  i^i 
Haus )  C_  Haus
16017ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 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 )
)
161159, 160sseldi 3439 . . . . . . . . . . . . . . . . . . . 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 )
162 df-ima 4835 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  =  ran  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) )
163 resres 5105 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) )  =  ( 2nd  |`  (
( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
) )
164 inss2 3659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( (
s  X.  k ) 
\  x )
165164, 121sstri 3450 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( s  X.  k )
166 ssres2 5119 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd  |`  ( ( U. R  X.  U. S )  i^i  ( ( s  X.  k )  \  x
) ) )  C_  ( 2nd  |`  ( s  X.  k ) )
168163, 167eqsstri 3471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) ) 
C_  ( 2nd  |`  (
s  X.  k ) )
169 rnss 5051 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
170168, 169ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  (
( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) ) 
C_  ran  ( 2nd  |`  ( s  X.  k
) )
171162, 170eqsstri 3471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  ran  ( 2nd  |`  ( s  X.  k
) )
172 f2ndres 6806 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2nd  |`  ( s  X.  k
) ) : ( s  X.  k ) --> k
173 frn 5719 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2nd  |`  ( s  X.  k ) ) : ( s  X.  k
) --> k  ->  ran  ( 2nd  |`  ( s  X.  k ) )  C_  k )
174172, 173ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ran  ( 2nd  |`  ( s  X.  k ) )  C_  k
175171, 174sstri 3450 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  k
176175, 78syl5ss 3452 . . . . . . . . . . . . . . . . . . . 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 )
17714ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 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 ) )
178153, 20sylib 196 . . . . . . . . . . . . . . . . . . . . . 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 ) )
179 tx2cn 20401 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  (TopOn `  U. R )  /\  S  e.  (TopOn `  U. S ) )  ->  ( 2nd  |`  ( U. R  X.  U. S ) )  e.  ( ( R  tX  S )  Cn  S
) )
180177, 178, 179syl2anc 659 . . . . . . . . . . . . . . . . . . . . 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 ) )
18128ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 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 )
182121a1i 11 . . . . . . . . . . . . . . . . . . . . . . 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
) )
183 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
184 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  k  e. 
_V
185183, 184xpex 6585 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  X.  k )  e. 
_V
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . 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 )
187 restabs 19957 . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
188181, 182, 186, 187syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
18966adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
190160, 5syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
191183a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
192 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
193 txrest 20422 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
194189, 190, 191, 192, 193syl22anc 1231 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195 simprr3 1047 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
196195adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
197 simprr 758 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
198 txcmp 20434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Rt  s )  e. 
Comp  /\  ( St  k )  e.  Comp )  ->  (
( Rt  s )  tX  ( St  k ) )  e.  Comp )
199196, 197, 198syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 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 )
200194, 199eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . 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 )
201 difin 3686 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  X.  k ) 
\  ( ( s  X.  k )  i^i  x ) )  =  ( ( s  X.  k )  \  x
)
20276, 78, 122syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
203189, 153, 26syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
204202, 203sseqtrd 3477 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
20529restuni 19954 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
206181, 204, 205syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
207206difeq1d 3559 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
208201, 207syl5eqr 2457 . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
209 resttop 19952 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( R  tX  S
)  e.  Top  /\  ( s  X.  k
)  e.  _V )  ->  ( ( R  tX  S )t  ( s  X.  k ) )  e. 
Top )
210181, 185, 209sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
211 incom 3631 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  X.  k )  i^i  x )  =  ( x  i^i  (
s  X.  k ) )
21223ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
213 kgeni 20328 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
214212, 200, 213syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
215211, 214syl5eqel 2494 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. (
( R  tX  S
)t  ( s  X.  k
) )  =  U. ( ( R  tX  S )t  ( s  X.  k ) )
217216opncld 19824 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
218210, 215, 217syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
219208, 218eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
220 cmpcld 20193 . . . . . . . . . . . . . . . . . . . . . . 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 )
221200, 219, 220syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 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 )
222188, 221eqeltrrd 2491 . . . . . . . . . . . . . . . . . . . . 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 )
223 imacmp 20188 . . . . . . . . . . . . . . . . . . . . 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 )
224180, 222, 223syl2anc 659 . . . . . . . . . . . . . . . . . . . 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 )
22519hauscmp 20198 . . . . . . . . . . . . . . . . . . . 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 )
)
226161, 176, 224, 225syl3anc 1230 . . . . . . . . . . . . . . . . . . 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
) )
227175a1i 11 . . . . . . . . . . . . . . . . . . 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 )
22819restcldi 19965 . . . . . . . . . . . . . . . . . . 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 ) ) )
22978, 226, 227, 228syl3anc 1230 . . . . . . . . . . . . . . . . . 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 ) ) )
230158, 229eqeltrrd 2491 . . . . . . . . . . . . . . . . 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 ) ) )
231 resttop 19952 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  e.  Top  /\  k  e.  ~P U. S
)  ->  ( St  k
)  e.  Top )
232153, 192, 231syl2anc 659 . . . . . . . . . . . . . . . . . 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 )
233 inss1 3658 . . . . . . . . . . . . . . . . . . 19  |-  ( k  i^i  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x } )  C_  k
234233, 155syl5sseq 3489 . . . . . . . . . . . . . . . . . 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 ) )
235 eqid 2402 . . . . . . . . . . . . . . . . . . 19  |-  U. ( St  k )  =  U. ( St  k )
236235isopn2 19823 . . . . . . . . . . . . . . . . . 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 ) ) ) )
237232, 234, 236syl2anc 659 . . . . . . . . . . . . . . . . 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 ) ) ) )
238230, 237mpbird 232 . . . . . . . . . . . . . . . 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 ) )
23971, 238syl5eqel 2494 . . . . . . . . . . . . . . 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 ) )
240239expr 613 . . . . . . . . . . . . . 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 ) ) )
241240ralrimiva 2817 . . . . . . . . . . . . 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 ) ) )
24267, 20sylib 196 . . . . . . . . . . . . . 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 ) )
243 elkgen 20327 . . . . . . . . . . . . . 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 ) ) ) ) )
244242, 243syl 17 . . . . . . . . . . . . 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 ) ) ) ) )
24570, 241, 244mpbir2and 923 . . . . . . . . . . . 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
) )
24617adantr 463 . . . . . . . . . . . . . 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 ) )
247246, 3syl 17 . . . . . . . . . . . . 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 )
248 kgenidm 20338 . . . . . . . . . . . . 13  |-  ( S  e.  ran 𝑘Gen  ->  (𝑘Gen `  S
)  =  S )
249247, 248syl 17 . . . . . . . . . . . 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 )
250245, 249eleqtrd 2492 . . . . . . . . . . 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 )
251 txopn 20393 . . . . . . . . . . 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 ) )
25266, 67, 68, 250, 251syl22anc 1231 . . . . . . . . . 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 ) )
25358adantr 463 . . . . . . . . . . 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
) >. )
254 simprr1 1045 . . . . . . . . . . . 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 )
25535adantr 463 . . . . . . . . . . . . 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
)  e.  U. S
)
256 relxp 4930 . . . . . . . . . . . . . . 15  |-  Rel  (
s  X.  { ( 2nd `  y ) } )
257256a1i 11 . . . . . . . . . . . . . 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