Theorem txkgen 21455

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

Assertion

Ref	Expression
txkgen	|- ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) -> ( R tX S ) e. ran 𝑘Gen )

Proof of Theorem txkgen

Dummy variables a b k s t u x y v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nllytop 21276	. . 3 |- ( R e. 𝑛Locally Comp -> R e. Top )
2		elinel1 3799	. . . 4 |- ( S e. ( ran 𝑘Gen i^i Haus ) -> S e. ran 𝑘Gen )
3		kgentop 21345	. . . 4 |- ( S e. ran 𝑘Gen -> S e. Top )
4	2, 3	syl 17	. . 3 |- ( S e. ( ran 𝑘Gen i^i Haus ) -> S e. Top )
5		txtop 21372	. . 3 |- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
6	1, 4, 5	syl2an 494	. 2 |- ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) -> ( R tX S ) e. Top )
7		simplll 798	. . . . . . . 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 )
8		eqid 2622	. . . . . . . . . 10 |- ( t e. U. R |-> <. t , ( 2nd ` y ) >. ) = ( t e. U. R |-> <. t , ( 2nd ` y ) >. )
9	8	mptpreima 5628	. . . . . . . . 9 |- ( `' ( t e. U. R |-> <. t , ( 2nd ` y ) >. ) " x ) = { t e. U. R | <. t , ( 2nd ` y ) >. e. x }
10	1	ad3antrrr 766	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> R e. Top )
11		eqid 2622	. . . . . . . . . . . . . . 15 |- U. R = U. R
12	11	toptopon 20722	. . . . . . . . . . . . . 14 |- ( R e. Top <-> R e. (TopOn ` U. R ) )
13	10, 12	sylib 208	. . . . . . . . . . . . 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 ) )
14		idcn 21061	. . . . . . . . . . . . 13 |- ( R e. (TopOn ` U. R ) -> ( _I |` U. R ) e. ( R Cn R ) )
15	13, 14	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> ( _I |` U. R ) e. ( R Cn R ) )
16		simpllr 799	. . . . . . . . . . . . . . 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 ) )
17	16, 4	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> S e. Top )
18		eqid 2622	. . . . . . . . . . . . . . 15 |- U. S = U. S
19	18	toptopon 20722	. . . . . . . . . . . . . 14 |- ( S e. Top <-> S e. (TopOn ` U. S ) )
20	17, 19	sylib 208	. . . . . . . . . . . . 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 ) )
21		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> y e. x )
22		simplr 792	. . . . . . . . . . . . . . . 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 ) ) )
23		elunii 4441	. . . . . . . . . . . . . . . 16 |- ( ( y e. x /\ x e. (𝑘Gen ` ( R tX S ) ) ) -> y e. U. (𝑘Gen ` ( R tX S ) ) )
24	21, 22, 23	syl2anc 693	. . . . . . . . . . . . . . 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 ) ) )
25	11, 18	txuni 21395	. . . . . . . . . . . . . . . . 17 |- ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
26	10, 17, 25	syl2anc 693	. . . . . . . . . . . . . . . 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 ) )
27	10, 17, 5	syl2anc 693	. . . . . . . . . . . . . . . . 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 )
28		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- U. ( R tX S ) = U. ( R tX S )
29	28	kgenuni 21342	. . . . . . . . . . . . . . . . 17 |- ( ( R tX S ) e. Top -> U. ( R tX S ) = U. (𝑘Gen ` ( R tX S ) ) )
30	27, 29	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> U. ( R tX S ) = U. (𝑘Gen ` ( R tX S ) ) )
31	26, 30	eqtrd 2656	. . . . . . . . . . . . . . 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 ) ) )
32	24, 31	eleqtrrd 2704	. . . . . . . . . . . . . 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 ) )
33		xp2nd 7199	. . . . . . . . . . . . . 14 |- ( y e. ( U. R X. U. S ) -> ( 2nd ` y ) e. U. S )
34	32, 33	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> ( 2nd ` y ) e. U. S )
35		cnconst2 21087	. . . . . . . . . . . . 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 ) )
36	13, 20, 34, 35	syl3anc 1326	. . . . . . . . . . . 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 ) )
37		fvresi 6439	. . . . . . . . . . . . . . . 16 |- ( t e. U. R -> ( ( _I |` U. R ) ` t ) = t )
38		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( 2nd ` y ) e. _V
39	38	fvconst2 6469	. . . . . . . . . . . . . . . 16 |- ( t e. U. R -> ( ( U. R X. { ( 2nd ` y ) } ) ` t ) = ( 2nd ` y ) )
40	37, 39	opeq12d 4410	. . . . . . . . . . . . . . 15 |- ( t e. U. R -> <. ( ( _I |` U. R ) ` t ) , ( ( U. R X. { ( 2nd ` y ) } ) ` t ) >. = <. t , ( 2nd ` y ) >. )
41	40	mpteq2ia 4740	. . . . . . . . . . . . . 14 |- ( t e. U. R |-> <. ( ( _I |` U. R ) ` t ) , ( ( U. R X. { ( 2nd ` y ) } ) ` t ) >. ) = ( t e. U. R |-> <. t , ( 2nd ` y ) >. )
42	41	eqcomi 2631	. . . . . . . . . . . . 13 |- ( t e. U. R |-> <. t , ( 2nd ` y ) >. ) = ( t e. U. R |-> <. ( ( _I |` U. R ) ` t ) , ( ( U. R X. { ( 2nd ` y ) } ) ` t ) >. )
43	11, 42	txcnmpt 21427	. . . . . . . . . . . 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 ) ) )
44	15, 36, 43	syl2anc 693	. . . . . . . . . . 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 ) ) )
45		llycmpkgen 21355	. . . . . . . . . . . . 13 |- ( R e. 𝑛Locally Comp -> R e. ran 𝑘Gen )
46	45	ad3antrrr 766	. . . . . . . . . . . 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 )
47	6	ad2antrr 762	. . . . . . . . . . . 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 )
48		kgencn3 21361	. . . . . . . . . . . 12 |- ( ( R e. ran 𝑘Gen /\ ( R tX S ) e. Top ) -> ( R Cn ( R tX S ) ) = ( R Cn (𝑘Gen ` ( R tX S ) ) ) )
49	46, 47, 48	syl2anc 693	. . . . . . . . . . 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 ) ) ) )
50	44, 49	eleqtrd 2703	. . . . . . . . . 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 ) ) ) )
51		cnima 21069	. . . . . . . . . 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 )
52	50, 22, 51	syl2anc 693	. . . . . . . . 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 )
53	9, 52	syl5eqelr 2706	. . . . . . . 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 )
54		xp1st 7198	. . . . . . . . . 10 |- ( y e. ( U. R X. U. S ) -> ( 1st ` y ) e. U. R )
55	32, 54	syl 17	. . . . . . . . 9 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> ( 1st ` y ) e. U. R )
56		1st2nd2 7205	. . . . . . . . . . 11 |- ( y e. ( U. R X. U. S ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
57	32, 56	syl 17	. . . . . . . . . 10 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
58	57, 21	eqeltrrd 2702	. . . . . . . . 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 )
59		opeq1 4402	. . . . . . . . . . 11 |- ( t = ( 1st ` y ) -> <. t , ( 2nd ` y ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
60	59	eleq1d 2686	. . . . . . . . . 10 |- ( t = ( 1st ` y ) -> ( <. t , ( 2nd ` y ) >. e. x <-> <. ( 1st ` y ) , ( 2nd ` y ) >. e. x ) )
61	60	elrab 3363	. . . . . . . . 9 |- ( ( 1st ` y ) e. { t e. U. R | <. t , ( 2nd ` y ) >. e. x } <-> ( ( 1st ` y ) e. U. R /\ <. ( 1st ` y ) , ( 2nd ` y ) >. e. x ) )
62	55, 58, 61	sylanbrc 698	. . . . . . . 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 } )
63		nlly2i 21279	. . . . . . . 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 /\ ( R ↾t s ) e. Comp ) )
64	7, 53, 62, 63	syl3anc 1326	. . . . . . 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 /\ ( R ↾t s ) e. Comp ) )
65	10	adantr 481	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> R e. Top )
66	17	adantr 481	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> S e. Top )
67		simprlr 803	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> u e. R )
68		ssrab2 3687	. . . . . . . . . . . . . 14 |- { v e. U. S | ( s X. { v } ) C_ x } C_ U. S
69	68	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) -> { v e. U. S | ( s X. { v } ) C_ x } C_ U. S )
70		incom 3805	. . . . . . . . . . . . . . . 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 } )
71		simprll 802	. . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } )
72	71	elpwid 4170	. . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> s C_ { t e. U. R | <. t , ( 2nd ` y ) >. e. x } )
73		ssrab2 3687	. . . . . . . . . . . . . . . . . . . . . 22 |- { t e. U. R | <. t , ( 2nd ` y ) >. e. x } C_ U. R
74	72, 73	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> s C_ U. R )
75	74	adantr 481	. . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> s C_ U. R )
76		elpwi 4168	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. ~P U. S -> k C_ U. S )
77	76	ad2antrl 764	. . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> k C_ U. S )
78		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t e. ( ( s X. k ) \ x ) <-> ( t e. ( s X. k ) /\ -. t e. x ) )
79	78	anbi1i 731	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
80		anass 681	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
81	79, 80	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
82	81	rexbii2 3039	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
83		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -. t e. x /\ ( ( 2nd |` ( U. R X. U. S ) ) ` t ) = b ) <-> ( ( ( 2nd |` ( U. R X. U. S ) ) ` t ) = b /\ -. t e. x ) )
84		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( t = <. a , u >. -> ( ( 2nd |` ( U. R X. U. S ) ) ` t ) = ( ( 2nd |` ( U. R X. U. S ) ) ` <. a , u >. ) )
85	84	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t = <. a , u >. -> ( ( ( 2nd |` ( U. R X. U. S ) ) ` t ) = b <-> ( ( 2nd |` ( U. R X. U. S ) ) ` <. a , u >. ) = b ) )
86		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( t = <. a , u >. -> ( t e. x <-> <. a , u >. e. x ) )
87	86	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t = <. a , u >. -> ( -. t e. x <-> -. <. a , u >. e. x ) )
88	85, 87	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
89	83, 88	syl5bb 272	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
90	89	rexxp 5264	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
91	82, 90	bitri 264	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
92		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( s C_ U. R /\ k C_ U. S ) -> s C_ U. R )
93	92	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( s C_ U. R /\ k C_ U. S ) /\ a e. s ) -> a e. U. R )
94	93	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( s C_ U. R /\ k C_ U. S ) /\ a e. s ) /\ u e. k ) -> a e. U. R )
95		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( s C_ U. R /\ k C_ U. S ) /\ a e. s ) -> k C_ U. S )
96	95	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( s C_ U. R /\ k C_ U. S ) /\ a e. s ) /\ u e. k ) -> u e. U. S )
97	94, 96	opelxpd 5149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( s C_ U. R /\ k C_ U. S ) /\ a e. s ) /\ u e. k ) -> <. a , u >. e. ( U. R X. U. S ) )
98	97	fvresd 6208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 >. ) )
99		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- a e. _V
100		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- u e. _V
101	99, 100	op2nd 7177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 2nd ` <. a , u >. ) = u
102	98, 101	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( s C_ U. R /\ k C_ U. S ) /\ a e. s ) /\ u e. k ) -> ( ( 2nd |` ( U. R X. U. S ) ) ` <. a , u >. ) = u )
103	102	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
104	103	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
105	104	rexbidva 3049	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
106		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( u = b -> <. a , u >. = <. a , b >. )
107	106	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( u = b -> ( <. a , u >. e. x <-> <. a , b >. e. x ) )
108	107	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( u = b -> ( -. <. a , u >. e. x <-> -. <. a , b >. e. x ) )
109	108	ceqsrexbv 3337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( E. u e. k ( u = b /\ -. <. a , u >. e. x ) <-> ( b e. k /\ -. <. a , b >. e. x ) )
110	105, 109	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
111	110	rexbidva 3049	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
112		r19.42v 3092	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( E. a e. s ( b e. k /\ -. <. a , b >. e. x ) <-> ( b e. k /\ E. a e. s -. <. a , b >. e. x ) )
113	111, 112	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
114	91, 113	syl5bb 272	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
115		f2ndres 7191	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 2nd |` ( U. R X. U. S ) ) : ( U. R X. U. S ) --> U. S
116		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
117	115, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2nd |` ( U. R X. U. S ) ) Fn ( U. R X. U. S )
118		difss 3737	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s X. k ) \ x ) C_ ( s X. k )
119		xpss12 5225	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s C_ U. R /\ k C_ U. S ) -> ( s X. k ) C_ ( U. R X. U. S ) )
120	118, 119	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( s C_ U. R /\ k C_ U. S ) -> ( ( s X. k ) \ x ) C_ ( U. R X. U. S ) )
121		fvelimab 6253	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
122	117, 120, 121	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 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 ) )
123		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . 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 } ) )
124		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( s C_ U. R /\ k C_ U. S ) -> k C_ U. S )
125	124	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( s C_ U. R /\ k C_ U. S ) /\ b e. k ) -> b e. U. S )
126		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( v = b -> { v } = { b } )
127	126	xpeq2d 5139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( v = b -> ( s X. { v } ) = ( s X. { b } ) )
128	127	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( v = b -> ( ( s X. { v } ) C_ x <-> ( s X. { b } ) C_ x ) )
129		dfss3 3592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( s X. { b } ) C_ x <-> A. k e. ( s X. { b } ) k e. x )
130		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( k = <. a , t >. -> ( k e. x <-> <. a , t >. e. x ) )
131	130	ralxp 5263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( A. k e. ( s X. { b } ) k e. x <-> A. a e. s A. t e. { b } <. a , t >. e. x )
132		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- b e. _V
133		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( t = b -> <. a , t >. = <. a , b >. )
134	133	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( t = b -> ( <. a , t >. e. x <-> <. a , b >. e. x ) )
135	132, 134	ralsn 4222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( A. t e. { b } <. a , t >. e. x <-> <. a , b >. e. x )
136	135	ralbii 2980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( A. a e. s A. t e. { b } <. a , t >. e. x <-> A. a e. s <. a , b >. e. x )
137	129, 131, 136	3bitri 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( s X. { b } ) C_ x <-> A. a e. s <. a , b >. e. x )
138	128, 137	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( v = b -> ( ( s X. { v } ) C_ x <-> A. a e. s <. a , b >. e. x ) )
139	138	elrab3 3364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( b e. U. S -> ( b e. { v e. U. S | ( s X. { v } ) C_ x } <-> A. a e. s <. a , b >. e. x ) )
140	125, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( s C_ U. R /\ k C_ U. S ) /\ b e. k ) -> ( b e. { v e. U. S | ( s X. { v } ) C_ x } <-> A. a e. s <. a , b >. e. x ) )
141	140	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
142		rexnal 2995	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( E. a e. s -. <. a , b >. e. x <-> -. A. a e. s <. a , b >. e. x )
143	141, 142	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
144	143	pm5.32da 673	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
145	123, 144	syl5bb 272	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
146	114, 122, 145	3bitr4d 300	. . . . . . . . . . . . . . . . . . . . 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 } ) ) )
147	146	eqrdv 2620	. . . . . . . . . . . . . . . . . . . 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 } ) )
148	75, 77, 147	syl2anc 693	. . . . . . . . . . . . . . . . . . 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 /\ ( 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 } ) )
149		difin 3861	. . . . . . . . . . . . . . . . . . . 20 |- ( k \ ( k i^i { v e. U. S | ( s X. { v } ) C_ x } ) ) = ( k \ { v e. U. S | ( s X. { v } ) C_ x } )
150	66	adantr 481	. . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> S e. Top )
151	18	restuni 20966	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S e. Top /\ k C_ U. S ) -> k = U. ( S ↾t k ) )
152	150, 77, 151	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> k = U. ( S ↾t k ) )
153	152	difeq1d 3727	. . . . . . . . . . . . . . . . . . . 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 /\ ( 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 } ) ) )
154	149, 153	syl5eqr 2670	. . . . . . . . . . . . . . . . . . 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 /\ ( 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 } ) ) )
155	148, 154	eqtrd 2656	. . . . . . . . . . . . . . . . . 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 /\ ( 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 } ) ) )
156	16	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> S e. ( ran 𝑘Gen i^i Haus ) )
157	156	elin2d 3803	. . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> S e. Haus )
158		df-ima 5127	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2nd |` ( U. R X. U. S ) ) " ( ( s X. k ) \ x ) ) = ran ( ( 2nd |` ( U. R X. U. S ) ) |` ( ( s X. k ) \ x ) )
159		resres 5409	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 2nd |` ( U. R X. U. S ) ) |` ( ( s X. k ) \ x ) ) = ( 2nd |` ( ( U. R X. U. S ) i^i ( ( s X. k ) \ x ) ) )
160		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( U. R X. U. S ) i^i ( ( s X. k ) \ x ) ) C_ ( ( s X. k ) \ x )
161	160, 118	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( U. R X. U. S ) i^i ( ( s X. k ) \ x ) ) C_ ( s X. k )
162		ssres2 5425	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
163	161, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2nd |` ( ( U. R X. U. S ) i^i ( ( s X. k ) \ x ) ) ) C_ ( 2nd |` ( s X. k ) )
164	159, 163	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 2nd |` ( U. R X. U. S ) ) |` ( ( s X. k ) \ x ) ) C_ ( 2nd |` ( s X. k ) )
165		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
166	164, 165	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 |- ran ( ( 2nd |` ( U. R X. U. S ) ) |` ( ( s X. k ) \ x ) ) C_ ran ( 2nd |` ( s X. k ) )
167	158, 166	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2nd |` ( U. R X. U. S ) ) " ( ( s X. k ) \ x ) ) C_ ran ( 2nd |` ( s X. k ) )
168		f2ndres 7191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2nd |` ( s X. k ) ) : ( s X. k ) --> k
169		frn 6053	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2nd |` ( s X. k ) ) : ( s X. k ) --> k -> ran ( 2nd |` ( s X. k ) ) C_ k )
170	168, 169	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ran ( 2nd |` ( s X. k ) ) C_ k
171	167, 170	sstri 3612	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2nd |` ( U. R X. U. S ) ) " ( ( s X. k ) \ x ) ) C_ k
172	171, 77	syl5ss 3614	. . . . . . . . . . . . . . . . . . . 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 /\ ( 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 )
173	13	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> R e. (TopOn ` U. R ) )
174	150, 19	sylib 208	. . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> S e. (TopOn ` U. S ) )
175		tx2cn 21413	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( R e. (TopOn ` U. R ) /\ S e. (TopOn ` U. S ) ) -> ( 2nd |` ( U. R X. U. S ) ) e. ( ( R tX S ) Cn S ) )
176	173, 174, 175	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) )
177	27	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( R tX S ) e. Top )
178	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( ( s X. k ) \ x ) C_ ( s X. k ) )
179		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- s e. _V
180		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- k e. _V
181	179, 180	xpex 6962	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s X. k ) e. _V
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( s X. k ) e. _V )
183		restabs 20969	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
184	177, 178, 182, 183	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
185	65	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> R e. Top )
186	156, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> S e. Top )
187	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> s e. _V )
188		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> k e. ~P U. S )
189		txrest 21434	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 ) ) )
190	185, 186, 187, 188, 189	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
191		simprr3 1111	. . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( R ↾t s ) e. Comp )
192	191	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( R ↾t s ) e. Comp )
193		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( S ↾t k ) e. Comp )
194		txcmp 21446	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( R ↾t s ) e. Comp /\ ( S ↾t k ) e. Comp ) -> ( ( R ↾t s ) tX ( S ↾t k ) ) e. Comp )
195	192, 193, 194	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( ( R ↾t s ) tX ( S ↾t k ) ) e. Comp )
196	190, 195	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( ( R tX S ) ↾t ( s X. k ) ) e. Comp )
197		difin 3861	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( s X. k ) \ ( ( s X. k ) i^i x ) ) = ( ( s X. k ) \ x )
198	75, 77, 119	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( s X. k ) C_ ( U. R X. U. S ) )
199	185, 150, 25	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( U. R X. U. S ) = U. ( R tX S ) )
200	198, 199	sseqtrd 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( s X. k ) C_ U. ( R tX S ) )
201	28	restuni 20966	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
202	177, 200, 201	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
203	202	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
204	197, 203	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
205		resttop 20964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( R tX S ) e. Top /\ ( s X. k ) e. _V ) -> ( ( R tX S ) ↾t ( s X. k ) ) e. Top )
206	177, 181, 205	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( ( R tX S ) ↾t ( s X. k ) ) e. Top )
207		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( s X. k ) i^i x ) = ( x i^i ( s X. k ) )
208	22	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> x e. (𝑘Gen ` ( R tX S ) ) )
209		kgeni 21340	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
210	208, 196, 209	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
211	207, 210	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
212		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U. ( ( R tX S ) ↾t ( s X. k ) ) = U. ( ( R tX S ) ↾t ( s X. k ) )
213	212	opncld 20837	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
214	206, 211, 213	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) ) )
215	204, 214	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) ) )
216		cmpcld 21205	. . . . . . . . . . . . . . . . . . . . . . 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 )
217	196, 215, 216	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 )
218	184, 217	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . 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 /\ ( 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 )
219		imacmp 21200	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 )
220	176, 218, 219	syl2anc 693	. . . . . . . . . . . . . . . . . . . 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 /\ ( 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 )
221	18	hauscmp 21210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) )
222	157, 172, 220, 221	syl3anc 1326	. . . . . . . . . . . . . . . . . . 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 /\ ( 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 ) )
223	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( 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 )
224	18	restcldi 20977	. . . . . . . . . . . . . . . . . . 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 ` ( S ↾t k ) ) )
225	77, 222, 223, 224	syl3anc 1326	. . . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
226	155, 225	eqeltrrd 2702	. . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) )
227		resttop 20964	. . . . . . . . . . . . . . . . . . 19 |- ( ( S e. Top /\ k e. ~P U. S ) -> ( S ↾t k ) e. Top )
228	150, 188, 227	syl2anc 693	. . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ ( k e. ~P U. S /\ ( S ↾t k ) e. Comp ) ) -> ( S ↾t k ) e. Top )
229		inss1 3833	. . . . . . . . . . . . . . . . . . 19 |- ( k i^i { v e. U. S | ( s X. { v } ) C_ x } ) C_ k
230	229, 152	syl5sseq 3653	. . . . . . . . . . . . . . . . . 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 /\ ( 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 ) )
231		eqid 2622	. . . . . . . . . . . . . . . . . . 19 |- U. ( S ↾t k ) = U. ( S ↾t k )
232	231	isopn2 20836	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
233	228, 230, 232	syl2anc 693	. . . . . . . . . . . . . . . . 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 /\ ( 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 ) ) ) )
234	226, 233	mpbird 247	. . . . . . . . . . . . . . . 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 /\ ( 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 ) )
235	70, 234	syl5eqel 2705	. . . . . . . . . . . . . . 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 /\ ( 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 ) )
236	235	expr 643	. . . . . . . . . . . . . 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 /\ ( 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 ) ) )
237	236	ralrimiva 2966	. . . . . . . . . . . . 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 /\ ( 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 ) ) )
238	66, 19	sylib 208	. . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> S e. (TopOn ` U. S ) )
239		elkgen 21339	. . . . . . . . . . . . . 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 ( ( S ↾t k ) e. Comp -> ( { v e. U. S | ( s X. { v } ) C_ x } i^i k ) e. ( S ↾t k ) ) ) ) )
240	238, 239	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t 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 ( ( S ↾t k ) e. Comp -> ( { v e. U. S | ( s X. { v } ) C_ x } i^i k ) e. ( S ↾t k ) ) ) ) )
241	69, 237, 240	mpbir2and 957	. . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> { v e. U. S | ( s X. { v } ) C_ x } e. (𝑘Gen ` S ) )
242	16	adantr 481	. . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> S e. ( ran 𝑘Gen i^i Haus ) )
243	242, 2	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) -> S e. ran 𝑘Gen )
244		kgenidm 21350	. . . . . . . . . . . . 13 |- ( S e. ran 𝑘Gen -> (𝑘Gen ` S ) = S )
245	243, 244	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) -> (𝑘Gen ` S ) = S )
246	241, 245	eleqtrd 2703	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> { v e. U. S | ( s X. { v } ) C_ x } e. S )
247		txopn 21405	. . . . . . . . . . 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 ) )
248	65, 66, 67, 246, 247	syl22anc 1327	. . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( u X. { v e. U. S | ( s X. { v } ) C_ x } ) e. ( R tX S ) )
249	57	adantr 481	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
250		simprr1 1109	. . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( 1st ` y ) e. u )
251	34	adantr 481	. . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( 2nd ` y ) e. U. S )
252		relxp 5227	. . . . . . . . . . . . . . 15 |- Rel ( s X. { ( 2nd ` y ) } )
253	252	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) /\ ( ( s e. ~P { t e. U. R | <. t , ( 2nd ` y ) >. e. x } /\ u e. R ) /\ ( ( 1st ` y ) e. u /\ u C_ s /\ ( R ↾t s ) e. Comp ) ) ) -> Rel ( s X. { ( 2nd ` y ) } ) )
254		opelxp 5146	. . . . . . . . . . . . . . 15 |- ( <. a , b >. e. ( s X. { ( 2nd ` y ) } ) <-> ( a e. s /\ b e. { ( 2nd ` y ) } ) )
255	72	sselda 3603	. . . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ a e. s ) -> a e. { t e. U. R | <. t , ( 2nd ` y ) >. e. x } )
256		opeq1 4402	. . . . . . . . . . . . . . . . . . . . 21 |- ( t = a -> <. t , ( 2nd ` y ) >. = <. a , ( 2nd ` y ) >. )
257	256	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20 |- ( t = a -> ( <. t , ( 2nd ` y ) >. e. x <-> <. a , ( 2nd ` y ) >. e. x ) )
258	257	elrab 3363	. . . . . . . . . . . . . . . . . . 19 |- ( a e. { t e. U. R | <. t , ( 2nd ` y ) >. e. x } <-> ( a e. U. R /\ <. a , ( 2nd ` y ) >. e. x ) )
259	258	simprbi 480	. . . . . . . . . . . . . . . . . 18 |- ( a e. { t e. U. R | <. t , ( 2nd ` y ) >. e. x } -> <. a , ( 2nd ` y ) >. e. x )
260	255, 259	syl 17	. . . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ a e. s ) -> <. a , ( 2nd ` y ) >. e. x )
261		elsni 4194	. . . . . . . . . . . . . . . . . . 19 |- ( b e. { ( 2nd ` y ) } -> b = ( 2nd ` y ) )
262	261	opeq2d 4409	. . . . . . . . . . . . . . . . . 18 |- ( b e. { ( 2nd ` y ) } -> <. a , b >. = <. a , ( 2nd ` y ) >. )
263	262	eleq1d 2686	. . . . . . . . . . . . . . . . 17 |- ( b e. { ( 2nd ` y ) } -> ( <. a , b >. e. x <-> <. a , ( 2nd ` y ) >. e. x ) )
264	260, 263	syl5ibrcom 237	. . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ a e. s ) -> ( b e. { ( 2nd ` y ) } -> <. a , b >. e. x ) )
265	264	expimpd 629	. . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( ( a e. s /\ b e. { ( 2nd ` y ) } ) -> <. a , b >. e. x ) )
266	254, 265	syl5bi 232	. . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( <. a , b >. e. ( s X. { ( 2nd ` y ) } ) -> <. a , b >. e. x ) )
267	253, 266	relssdv 5212	. . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( s X. { ( 2nd ` y ) } ) C_ x )
268		sneq 4187	. . . . . . . . . . . . . . . 16 |- ( v = ( 2nd ` y ) -> { v } = { ( 2nd ` y ) } )
269	268	xpeq2d 5139	. . . . . . . . . . . . . . 15 |- ( v = ( 2nd ` y ) -> ( s X. { v } ) = ( s X. { ( 2nd ` y ) } ) )
270	269	sseq1d 3632	. . . . . . . . . . . . . 14 |- ( v = ( 2nd ` y ) -> ( ( s X. { v } ) C_ x <-> ( s X. { ( 2nd ` y ) } ) C_ x ) )
271	270	elrab 3363	. . . . . . . . . . . . 13 |- ( ( 2nd ` y ) e. { v e. U. S | ( s X. { v } ) C_ x } <-> ( ( 2nd ` y ) e. U. S /\ ( s X. { ( 2nd ` y ) } ) C_ x ) )
272	251, 267, 271	sylanbrc 698	. . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( 2nd ` y ) e. { v e. U. S | ( s X. { v } ) C_ x } )
273	250, 272	opelxpd 5149	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( u X. { v e. U. S | ( s X. { v } ) C_ x } ) )
274	249, 273	eqeltrd 2701	. . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> y e. ( u X. { v e. U. S | ( s X. { v } ) C_ x } ) )
275		relxp 5227	. . . . . . . . . . . 12 |- Rel ( u X. { v e. U. S | ( s X. { v } ) C_ x } )
276	275	a1i 11	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> Rel ( u X. { v e. U. S | ( s X. { v } ) C_ x } ) )
277		opelxp 5146	. . . . . . . . . . . 12 |- ( <. 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 } ) )
278	128	elrab 3363	. . . . . . . . . . . . . . 15 |- ( b e. { v e. U. S | ( s X. { v } ) C_ x } <-> ( b e. U. S /\ ( s X. { b } ) C_ x ) )
279	278	simprbi 480	. . . . . . . . . . . . . 14 |- ( b e. { v e. U. S | ( s X. { v } ) C_ x } -> ( s X. { b } ) C_ x )
280		simprr2 1110	. . . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> u C_ s )
281	280	sselda 3603	. . . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ a e. u ) -> a e. s )
282		vsnid 4209	. . . . . . . . . . . . . . 15 |- b e. { b }
283		opelxpi 5148	. . . . . . . . . . . . . . 15 |- ( ( a e. s /\ b e. { b } ) -> <. a , b >. e. ( s X. { b } ) )
284	281, 282, 283	sylancl 694	. . . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ a e. u ) -> <. a , b >. e. ( s X. { b } ) )
285		ssel 3597	. . . . . . . . . . . . . 14 |- ( ( s X. { b } ) C_ x -> ( <. a , b >. e. ( s X. { b } ) -> <. a , b >. e. x ) )
286	279, 284, 285	syl2imc 41	. . . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) /\ a e. u ) -> ( b e. { v e. U. S | ( s X. { v } ) C_ x } -> <. a , b >. e. x ) )
287	286	expimpd 629	. . . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( ( a e. u /\ b e. { v e. U. S | ( s X. { v } ) C_ x } ) -> <. a , b >. e. x ) )
288	277, 287	syl5bi 232	. . . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( <. a , b >. e. ( u X. { v e. U. S | ( s X. { v } ) C_ x } ) -> <. a , b >. e. x ) )
289	276, 288	relssdv 5212	. . . . . . . . . 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 /\ ( R ↾t s ) e. Comp ) ) ) -> ( u X. { v e. U. S | ( s X. { v } ) C_ x } ) C_ x )
290		eleq2 2690	. . . . . . . . . . . 12 |- ( 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 } ) ) )
291		sseq1 3626	. . . . . . . . . . . 12 |- ( 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 ) )
292	290, 291	anbi12d 747	. . . . . . . . . . 11 |- ( 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 ) ) )
293	292	rspcev 3309	. . . . . . . . . 10 |- ( ( ( 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 ) )
294	248, 274, 289, 293	syl12anc 1324	. . . . . . . . 9 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y 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 ) )
295	294	expr 643	. . . . . . . 8 |- ( ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y 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 ) ) )
296	295	rexlimdvva 3038	. . . . . . 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 /\ ( R ↾t s ) e. Comp ) -> E. t e. ( R tX S ) ( y e. t /\ t C_ x ) ) )
297	64, 296	mpd 15	. . . . . 6 |- ( ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) /\ y e. x ) -> E. t e. ( R tX S ) ( y e. t /\ t C_ x ) )
298	297	ralrimiva 2966	. . . . 5 |- ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) -> A. y e. x E. t e. ( R tX S ) ( y e. t /\ t C_ x ) )
299	6	adantr 481	. . . . . 6 |- ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) -> ( R tX S ) e. Top )
300		eltop2 20779	. . . . . 6 |- ( ( 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 ) ) )
301	299, 300	syl 17	. . . . 5 |- ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) -> ( x e. ( R tX S ) <-> A. y e. x E. t e. ( R tX S ) ( y e. t /\ t C_ x ) ) )
302	298, 301	mpbird 247	. . . 4 |- ( ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) /\ x e. (𝑘Gen ` ( R tX S ) ) ) -> x e. ( R tX S ) )
303	302	ex 450	. . 3 |- ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) -> ( x e. (𝑘Gen ` ( R tX S ) ) -> x e. ( R tX S ) ) )
304	303	ssrdv 3609	. 2 |- ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) -> (𝑘Gen ` ( R tX S ) ) C_ ( R tX S ) )
305		iskgen2 21351	. 2 |- ( ( R tX S ) e. ran 𝑘Gen <-> ( ( R tX S ) e. Top /\ (𝑘Gen ` ( R tX S ) ) C_ ( R tX S ) ) )
306	6, 304, 305	sylanbrc 698	1 |- ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) -> ( R tX S ) e. ran 𝑘Gen )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   <.cop 4183   U.cuni 4436   |-> cmpt 4729   _I cid 5023   X. cxp 5112   `'ccnv 5113   ran crn 5115   |` cres 5116   "cima 5117   Rel wrel 5119   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ↾_t crest 16081   Topctop 20698  TopOnctopon 20715   Clsdccld 20820   Cn ccn 21028   Hauscha 21112   Compccmp 21189  𝑛Locally cnlly 21268  𝑘Genckgen 21336   tX ctx 21363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-nlly 21270  df-kgen 21337  df-tx 21365

This theorem is referenced by: (None)