Metamath Proof Explorer

Theorem txkgen

Description: The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on S can also be replaced with either "compactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion txkgen 
|- ( ( R e. N-Locally Comp /\ S e. ( ran kGen i^i Haus ) ) -> ( R tX S ) e. ran kGen )

Proof

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