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

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