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

Theorem txkgen 17686
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 17538 . . 3  |-  ( R  e. 𝑛Locally 
Comp  ->  R  e.  Top )
2 inss1 3563 . . . . 5  |-  ( ran 𝑘Gen  i^i 
Haus )  C_  ran 𝑘Gen
32sseli 3346 . . . 4  |-  ( S  e.  ( ran 𝑘Gen  i^i  Haus )  ->  S  e.  ran 𝑘Gen )
4 kgentop 17576 . . . 4  |-  ( S  e.  ran 𝑘Gen  ->  S  e.  Top )
53, 4syl 16 . . 3  |-  ( S  e.  ( ran 𝑘Gen  i^i  Haus )  ->  S  e.  Top )
6 txtop 17603 . . 3  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( R  tX  S
)  e.  Top )
71, 5, 6syl2an 465 . 2  |-  ( ( R  e. 𝑛Locally  Comp  /\  S  e.  ( ran 𝑘Gen  i^i  Haus ) )  -> 
( R  tX  S
)  e.  Top )
8 simplll 736 . . . . . . . 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 2438 . . . . . . . . . 10  |-  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )  =  ( t  e. 
U. R  |->  <. t ,  ( 2nd `  y
) >. )
109mptpreima 5365 . . . . . . . . 9  |-  ( `' ( t  e.  U. R  |->  <. t ,  ( 2nd `  y )
>. ) " x )  =  { t  e. 
U. R  |  <. t ,  ( 2nd `  y
) >.  e.  x }
111ad3antrrr 712 . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . 15  |-  U. R  =  U. R
1312toptopon 17000 . . . . . . . . . . . . . 14  |-  ( R  e.  Top  <->  R  e.  (TopOn `  U. R ) )
1411, 13sylib 190 . . . . . . . . . . . . 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 17323 . . . . . . . . . . . . 13  |-  ( R  e.  (TopOn `  U. R )  ->  (  _I  |`  U. R )  e.  ( R  Cn  R ) )
1614, 15syl 16 . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . 15  |-  U. S  =  U. S
2019toptopon 17000 . . . . . . . . . . . . . 14  |-  ( S  e.  Top  <->  S  e.  (TopOn `  U. S ) )
2118, 20sylib 190 . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . 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 4022 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  x  /\  x  e.  (𝑘Gen `  ( R  tX  S ) ) )  ->  y  e.  U. (𝑘Gen `  ( R  tX  S ) ) )
2522, 23, 24syl2anc 644 . . . . . . . . . . . . . . 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 17626 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( U. R  X.  U. S )  =  U. ( R  tX  S ) )
2711, 18, 26syl2anc 644 . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . . . . 18  |-  U. ( R  tX  S )  = 
U. ( R  tX  S )
3029kgenuni 17573 . . . . . . . . . . . . . . . . 17  |-  ( ( R  tX  S )  e.  Top  ->  U. ( R  tX  S )  = 
U. (𝑘Gen `  ( R  tX  S ) ) )
3128, 30syl 16 . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . 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 2515 . . . . . . . . . . . . . 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 6379 . . . . . . . . . . . . . 14  |-  ( y  e.  ( U. R  X.  U. S )  -> 
( 2nd `  y
)  e.  U. S
)
3533, 34syl 16 . . . . . . . . . . . . 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 17349 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 5926 . . . . . . . . . . . . . . . 16  |-  ( t  e.  U. R  -> 
( (  _I  |`  U. R
) `  t )  =  t )
39 fvex 5744 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  y )  e.  _V
4039fvconst2 5949 . . . . . . . . . . . . . . . 16  |-  ( t  e.  U. R  -> 
( ( U. R  X.  { ( 2nd `  y
) } ) `  t )  =  ( 2nd `  y ) )
4138, 40opeq12d 3994 . . . . . . . . . . . . . . 15  |-  ( t  e.  U. R  ->  <. ( (  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.  =  <. t ,  ( 2nd `  y )
>. )
4241mpteq2ia 4293 . . . . . . . . . . . . . 14  |-  ( t  e.  U. R  |->  <.
( (  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.
)  =  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )
4342eqcomi 2442 . . . . . . . . . . . . 13  |-  ( t  e.  U. R  |->  <.
t ,  ( 2nd `  y ) >. )  =  ( t  e. 
U. R  |->  <. (
(  _I  |`  U. R
) `  t ) ,  ( ( U. R  X.  { ( 2nd `  y ) } ) `
 t ) >.
)
4412, 43txcnmpt 17658 . . . . . . . . . . . 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 644 . . . . . . . . . . 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 17586 . . . . . . . . . . . . 13  |-  ( R  e. 𝑛Locally 
Comp  ->  R  e.  ran 𝑘Gen )
4746ad3antrrr 712 . . . . . . . . . . . 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 708 . . . . . . . . . . . 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 17592 . . . . . . . . . . . 12  |-  ( ( R  e.  ran 𝑘Gen  /\  ( R  tX  S )  e. 
Top )  ->  ( R  Cn  ( R  tX  S ) )  =  ( R  Cn  (𝑘Gen `  ( R  tX  S ) ) ) )
5047, 48, 49syl2anc 644 . . . . . . . . . . 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 2514 . . . . . . . . . 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 17331 . . . . . . . . . 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 644 . . . . . . . . 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 2523 . . . . . . . 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 6378 . . . . . . . . . 10  |-  ( y  e.  ( U. R  X.  U. S )  -> 
( 1st `  y
)  e.  U. R
)
5633, 55syl 16 . . . . . . . . 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 6388 . . . . . . . . . . 11  |-  ( y  e.  ( U. R  X.  U. S )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
5833, 57syl 16 . . . . . . . . . 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 2513 . . . . . . . . 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 3986 . . . . . . . . . . 11  |-  ( t  =  ( 1st `  y
)  ->  <. t ,  ( 2nd `  y
) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
6160eleq1d 2504 . . . . . . . . . 10  |-  ( t  =  ( 1st `  y
)  ->  ( <. t ,  ( 2nd `  y
) >.  e.  x  <->  <. ( 1st `  y ) ,  ( 2nd `  y )
>.  e.  x ) )
6261elrab 3094 . . . . . . . . 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 647 . . . . . . . 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 17541 . . . . . . . 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 1185 . . . . . . 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 453 . . . . . . . . . . 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 453 . . . . . . . . . . 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 741 . . . . . . . . . . 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 3430 . . . . . . . . . . . . . 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 3535 . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . . . . . . . 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 3810 . . . . . . . . . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . . . . . . . . . . 22  |-  { t  e.  U. R  |  <. t ,  ( 2nd `  y ) >.  e.  x }  C_  U. R
7573, 74syl6ss 3362 . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . 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 3809 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ~P U. S  ->  k  C_  U. S )
7877ad2antrl 710 . . . . . . . . . . . . . . . . . . . 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 3332 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  ( ( s  X.  k )  \  x )  <->  ( t  e.  ( s  X.  k
)  /\  -.  t  e.  x ) )
8079anbi1i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 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 632 . . . . . . . . . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . . . . . . . . . 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 2736 . . . . . . . . . . . . . . . . . . . . . . . 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 439 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  <. a ,  u >.  ->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  ( ( 2nd  |`  ( U. R  X.  U. S
) ) `  <. a ,  u >. )
)
8685eqeq1d 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  <. a ,  u >.  ->  ( ( ( 2nd  |`  ( U. R  X.  U. S ) ) `  t )  =  b  <->  ( ( 2nd  |`  ( U. R  X.  U. S ) ) `
 <. a ,  u >. )  =  b ) )
87 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  <. a ,  u >.  ->  ( t  e.  x  <->  <. a ,  u >.  e.  x ) )
8887notbid 287 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  <. a ,  u >.  ->  ( -.  t  e.  x  <->  -.  <. a ,  u >.  e.  x
) )
8986, 88anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . . . . 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 250 . . . . . . . . . . . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . . . . . . . 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 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  s  C_  U. R
)
9493sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  a  e.  U. R )
9594adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  a  e.  U. R )
96 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  a  e.  s )  ->  k  C_ 
U. S )
9796sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( s  C_  U. R  /\  k  C_  U. S )  /\  a  e.  s )  /\  u  e.  k )  ->  u  e.  U. S )
98 opelxpi 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( a  e.  U. R  /\  u  e.  U. S
)  ->  <. a ,  u >.  e.  ( U. R  X.  U. S
) )
9995, 97, 98syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
a ,  u >.  e.  ( U. R  X.  U. S )  ->  (
( 2nd  |`  ( U. R  X.  U. S ) ) `  <. a ,  u >. )  =  ( 2nd `  <. a ,  u >. ) )
10199, 100syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  a  e. 
_V
103 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  u  e. 
_V
104102, 103op2nd 6358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2nd `  <. a ,  u >. )  =  u
105101, 104syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 687 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2724 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  b  ->  <. a ,  u >.  =  <. a ,  b >. )
110109eleq1d 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  =  b  ->  ( <. a ,  u >.  e.  x  <->  <. a ,  b
>.  e.  x ) )
111110notbid 287 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  =  b  ->  ( -.  <. a ,  u >.  e.  x  <->  -.  <. a ,  b >.  e.  x
) )
112111ceqsrexbv 3072 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. u  e.  k  ( u  =  b  /\  -.  <. a ,  u >.  e.  x )  <->  ( b  e.  k  /\  -.  <. a ,  b >.  e.  x
) )
113108, 112syl6bb 254 . . . . . . . . . . . . . . . . . . . . . . . . 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 2724 . . . . . . . . . . . . . . . . . . . . . . . 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 2864 . . . . . . . . . . . . . . . . . . . . . . . 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 254 . . . . . . . . . . . . . . . . . . . . . . 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 250 . . . . . . . . . . . . . . . . . . . . . 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 6371 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd  |`  ( U. R  X.  U. S ) ) : ( U. R  X.  U. S ) --> U. S
119 ffn 5593 . . . . . . . . . . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2nd  |`  ( U. R  X.  U. S ) )  Fn  ( U. R  X.  U. S )
121 difss 3476 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  X.  k ) 
\  x )  C_  ( s  X.  k
)
122 xpss12 4983 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( s  X.  k )  C_  ( U. R  X.  U. S
) )
123121, 122syl5ss 3361 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  ( ( s  X.  k )  \  x )  C_  ( U. R  X.  U. S
) )
124 fvelimab 5784 . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . . 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 3332 . . . . . . . . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  C_  U. R  /\  k  C_  U. S )  ->  k  C_  U. S
)
128127sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( s  C_  U. R  /\  k  C_  U. S
)  /\  b  e.  k )  ->  b  e.  U. S )
129 sneq 3827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  =  b  ->  { v }  =  { b } )
130129xpeq2d 4904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( v  =  b  ->  (
s  X.  { v } )  =  ( s  X.  { b } ) )
131130sseq1d 3377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( v  =  b  ->  (
( s  X.  {
v } )  C_  x 
<->  ( s  X.  {
b } )  C_  x ) )
132 dfss3 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( s  X.  { b } )  C_  x  <->  A. k  e.  ( s  X.  { b } ) k  e.  x
)
133 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  <. a ,  t
>.  ->  ( k  e.  x  <->  <. a ,  t
>.  e.  x ) )
134133ralxp 5018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. k  e.  ( s  X.  { b } ) k  e.  x  <->  A. a  e.  s  A. t  e.  { b } <. a ,  t >.  e.  x
)
135 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  b  e. 
_V
136 opeq2 3987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  b  ->  <. a ,  t >.  =  <. a ,  b >. )
137136eleq1d 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  b  ->  ( <. a ,  t >.  e.  x  <->  <. a ,  b
>.  e.  x ) )
138135, 137ralsn 3851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. t  e.  { b } <. a ,  t
>.  e.  x  <->  <. a ,  b >.  e.  x
)
139138ralbii 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. a  e.  s  A. t  e.  { b } <. a ,  t
>.  e.  x  <->  A. a  e.  s  <. a ,  b >.  e.  x
)
140132, 134, 1393bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  X.  { b } )  C_  x  <->  A. a  e.  s  <. a ,  b >.  e.  x
)
141131, 140syl6bb 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( v  =  b  ->  (
( s  X.  {
v } )  C_  x 
<-> 
A. a  e.  s 
<. a ,  b >.  e.  x ) )
142141elrab3 3095 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . 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 287 . . . . . . . . . . . . . . . . . . . . . . . . 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 2718 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. a  e.  s  -. 
<. a ,  b >.  e.  x  <->  -.  A. a  e.  s  <. a ,  b >.  e.  x
)
146144, 145syl6bbr 256 . . . . . . . . . . . . . . . . . . . . . . . 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 624 . . . . . . . . . . . . . . . . . . . . . . 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 250 . . . . . . . . . . . . . . . . . . . . . 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 278 . . . . . . . . . . . . . . . . . . . . 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 2436 . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . 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 3580 . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . 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 17228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  Top  /\  k  C_  U. S )  ->  k  =  U. ( St  k ) )
155153, 78, 154syl2anc 644 . . . . . . . . . . . . . . . . . . . . 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 3466 . . . . . . . . . . . . . . . . . . . 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 2484 . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . 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 3564 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 𝑘Gen  i^i 
Haus )  C_  Haus
16017ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 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 3348 . . . . . . . . . . . . . . . . . . . 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 4893 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) )  =  ran  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) )
163 resres 5161 . . . . . . . . . . . . . . . . . . . . . . . . 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 3564 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( (
s  X.  k ) 
\  x )
165164, 121sstri 3359 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( U. R  X.  U. S )  i^i  (
( s  X.  k
)  \  x )
)  C_  ( s  X.  k )
166 ssres2 5175 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd  |`  ( ( U. R  X.  U. S )  i^i  ( ( s  X.  k )  \  x
) ) )  C_  ( 2nd  |`  ( s  X.  k ) )
168163, 167eqsstri 3380 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) ) 
C_  ( 2nd  |`  (
s  X.  k ) )
169 rnss 5100 . . . . . . . . . . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  (
( 2nd  |`  ( U. R  X.  U. S ) )  |`  ( (
s  X.  k ) 
\  x ) ) 
C_  ran  ( 2nd  |`  ( s  X.  k
) )
171162, 170eqsstri 3380 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  ran  ( 2nd  |`  ( s  X.  k
) )
172 f2ndres 6371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2nd  |`  ( s  X.  k
) ) : ( s  X.  k ) --> k
173 frn 5599 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2nd  |`  ( s  X.  k ) ) : ( s  X.  k
) --> k  ->  ran  ( 2nd  |`  ( s  X.  k ) )  C_  k )
174172, 173ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ran  ( 2nd  |`  ( s  X.  k ) )  C_  k
175171, 174sstri 3359 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd  |`  ( U. R  X.  U. S ) ) " ( ( s  X.  k ) 
\  x ) ) 
C_  k
176175, 78syl5ss 3361 . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . 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 190 . . . . . . . . . . . . . . . . . . . . . 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 17644 . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . 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 2961 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
184 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  k  e. 
_V
185183, 184xpex 4992 . . . . . . . . . . . . . . . . . . . . . . . 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 17231 . . . . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . 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 17665 . . . . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . . . . 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 1008 . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . . . . . . . . . . . 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 17677 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Rt  s )  e. 
Comp  /\  ( St  k )  e.  Comp )  ->  (
( Rt  s )  tX  ( St  k ) )  e.  Comp )
199196, 197, 198syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . . . . . . . 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 3580 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  X.  k ) 
\  ( ( s  X.  k )  i^i  x ) )  =  ( ( s  X.  k )  \  x
)
20276, 78, 122syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3386 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17228 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3466 . . . . . . . . . . . . . . . . . . . . . . . . 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 2484 . . . . . . . . . . . . . . . . . . . . . . . 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 17226 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( R  tX  S
)  e.  Top  /\  ( s  X.  k
)  e.  _V )  ->  ( ( R  tX  S )t  ( s  X.  k ) )  e. 
Top )
210181, 185, 209sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . 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 3535 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  X.  k )  i^i  x )  =  ( x  i^i  (
s  X.  k ) )
21223ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17571 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2522 . . . . . . . . . . . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. (
( R  tX  S
)t  ( s  X.  k
) )  =  U. ( ( R  tX  S )t  ( s  X.  k ) )
217216opncld 17099 . . . . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . . . . . . . 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 17467 . . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . . 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 2513 . . . . . . . . . . . . . . . . . . . . 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 17462 . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . 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 17472 . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . 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 17239 . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . 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 2513 . . . . . . . . . . . . . . . . 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 17226 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  e.  Top  /\  k  e.  ~P U. S
)  ->  ( St  k
)  e.  Top )
232153, 192, 231syl2anc 644 . . . . . . . . . . . . . . . . . 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 3563 . . . . . . . . . . . . . . . . . . 19  |-  ( k  i^i  { v  e. 
U. S  |  ( s  X.  { v } )  C_  x } )  C_  k
234233, 155syl5sseq 3398 . . . . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . . . . . 19  |-  U. ( St  k )  =  U. ( St  k )
236235isopn2 17098 . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . 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 2522 . . . . . . . . . . . . . . 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 600 . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . 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 190 . . . . . . . . . . . . . 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 17570 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 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 890 . . . . . . . . . . . 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 453 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 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 17581 . . . . . . . . . . . . 13  |-  ( S  e.  ran 𝑘Gen  ->  (𝑘Gen `  S
)  =  S )
249247, 248syl 16 . . . . . . . . . . . 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 2514 . . . . . . . . . . 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 17636 . . . . . . . . . . 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 1186 . . . . . . . . . 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 453 . . . . . . . . . . 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 1006 . . . . . . . . . . . 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 453 . . . . . . . . . . . . 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 4985 . . . . . . . . . . . . . . 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 }