Theorem xkoinjcn 21490

Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.)

Hypothesis

Ref	Expression
xkoinjcn.3	|- F = ( x e. X |-> ( y e. Y |-> <. y , x >. ) )

Assertion

Ref	Expression
xkoinjcn	|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> F e. ( R Cn ( ( S tX R ) ^ko S ) ) )

Distinct variable groups:   x, y, R   x, S, y   x, Y, y   x, X, y

Allowed substitution hints:   F( x, y)

Proof of Theorem xkoinjcn

Dummy variables f k r v w z t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 792	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. X ) -> S e. (TopOn ` Y ) )
2	1	cnmptid 21464	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. X ) -> ( y e. Y |-> y ) e. ( S Cn S ) )
3		simpll 790	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. X ) -> R e. (TopOn ` X ) )
4		simpr 477	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. X ) -> x e. X )
5	1, 3, 4	cnmptc 21465	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. X ) -> ( y e. Y |-> x ) e. ( S Cn R ) )
6	1, 2, 5	cnmpt1t 21468	. . 3 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. X ) -> ( y e. Y |-> <. y , x >. ) e. ( S Cn ( S tX R ) ) )
7		xkoinjcn.3	. . 3 |- F = ( x e. X |-> ( y e. Y |-> <. y , x >. ) )
8	6, 7	fmptd 6385	. 2 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> F : X --> ( S Cn ( S tX R ) ) )
9		eqid 2622	. . . . . 6 |- U. S = U. S
10		eqid 2622	. . . . . 6 |- { w e. ~P U. S | ( S ↾t w ) e. Comp } = { w e. ~P U. S | ( S ↾t w ) e. Comp }
11		eqid 2622	. . . . . 6 |- ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) = ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } )
12	9, 10, 11	xkobval 21389	. . . . 5 |- ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) = { z | E. k e. ~P U. S E. v e. ( S tX R ) ( ( S ↾t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) }
13	12	abeq2i 2735	. . . 4 |- ( z e. ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) <-> E. k e. ~P U. S E. v e. ( S tX R ) ( ( S ↾t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) )
14		simpll 790	. . . . . . . . . . . 12 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) )
15	14, 6	sylan 488	. . . . . . . . . . 11 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> ( y e. Y |-> <. y , x >. ) e. ( S Cn ( S tX R ) ) )
16		imaeq1 5461	. . . . . . . . . . . . 13 |- ( f = ( y e. Y |-> <. y , x >. ) -> ( f " k ) = ( ( y e. Y |-> <. y , x >. ) " k ) )
17	16	sseq1d 3632	. . . . . . . . . . . 12 |- ( f = ( y e. Y |-> <. y , x >. ) -> ( ( f " k ) C_ v <-> ( ( y e. Y |-> <. y , x >. ) " k ) C_ v ) )
18	17	elrab3 3364	. . . . . . . . . . 11 |- ( ( y e. Y |-> <. y , x >. ) e. ( S Cn ( S tX R ) ) -> ( ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } <-> ( ( y e. Y |-> <. y , x >. ) " k ) C_ v ) )
19	15, 18	syl 17	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> ( ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } <-> ( ( y e. Y |-> <. y , x >. ) " k ) C_ v ) )
20		funmpt 5926	. . . . . . . . . . 11 |- Fun ( y e. Y |-> <. y , x >. )
21		simplrl 800	. . . . . . . . . . . . . . 15 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> k e. ~P U. S )
22	21	elpwid 4170	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> k C_ U. S )
23	14	simprd 479	. . . . . . . . . . . . . . 15 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> S e. (TopOn ` Y ) )
24		toponuni 20719	. . . . . . . . . . . . . . 15 |- ( S e. (TopOn ` Y ) -> Y = U. S )
25	23, 24	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> Y = U. S )
26	22, 25	sseqtr4d 3642	. . . . . . . . . . . . 13 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> k C_ Y )
27	26	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> k C_ Y )
28		dmmptg 5632	. . . . . . . . . . . . 13 |- ( A. y e. Y <. y , x >. e. _V -> dom ( y e. Y |-> <. y , x >. ) = Y )
29		opex 4932	. . . . . . . . . . . . . 14 |- <. y , x >. e. _V
30	29	a1i 11	. . . . . . . . . . . . 13 |- ( y e. Y -> <. y , x >. e. _V )
31	28, 30	mprg 2926	. . . . . . . . . . . 12 |- dom ( y e. Y |-> <. y , x >. ) = Y
32	27, 31	syl6sseqr 3652	. . . . . . . . . . 11 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> k C_ dom ( y e. Y |-> <. y , x >. ) )
33		funimass4 6247	. . . . . . . . . . 11 |- ( ( Fun ( y e. Y |-> <. y , x >. ) /\ k C_ dom ( y e. Y |-> <. y , x >. ) ) -> ( ( ( y e. Y |-> <. y , x >. ) " k ) C_ v <-> A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v ) )
34	20, 32, 33	sylancr 695	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> ( ( ( y e. Y |-> <. y , x >. ) " k ) C_ v <-> A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v ) )
35	27	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> z e. Y )
36		opeq1 4402	. . . . . . . . . . . . . . . 16 |- ( y = z -> <. y , x >. = <. z , x >. )
37		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( y e. Y |-> <. y , x >. ) = ( y e. Y |-> <. y , x >. )
38		opex 4932	. . . . . . . . . . . . . . . 16 |- <. z , x >. e. _V
39	36, 37, 38	fvmpt 6282	. . . . . . . . . . . . . . 15 |- ( z e. Y -> ( ( y e. Y |-> <. y , x >. ) ` z ) = <. z , x >. )
40	35, 39	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> ( ( y e. Y |-> <. y , x >. ) ` z ) = <. z , x >. )
41	40	eleq1d 2686	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> ( ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> <. z , x >. e. v ) )
42		vex 3203	. . . . . . . . . . . . . 14 |- x e. _V
43		opeq2 4403	. . . . . . . . . . . . . . 15 |- ( w = x -> <. z , w >. = <. z , x >. )
44	43	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( w = x -> ( <. z , w >. e. v <-> <. z , x >. e. v ) )
45	42, 44	ralsn 4222	. . . . . . . . . . . . 13 |- ( A. w e. { x } <. z , w >. e. v <-> <. z , x >. e. v )
46	41, 45	syl6bbr 278	. . . . . . . . . . . 12 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> ( ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> A. w e. { x } <. z , w >. e. v ) )
47	46	ralbidva 2985	. . . . . . . . . . 11 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> ( A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> A. z e. k A. w e. { x } <. z , w >. e. v ) )
48		dfss3 3592	. . . . . . . . . . . 12 |- ( ( k X. { x } ) C_ v <-> A. t e. ( k X. { x } ) t e. v )
49		eleq1 2689	. . . . . . . . . . . . 13 |- ( t = <. z , w >. -> ( t e. v <-> <. z , w >. e. v ) )
50	49	ralxp 5263	. . . . . . . . . . . 12 |- ( A. t e. ( k X. { x } ) t e. v <-> A. z e. k A. w e. { x } <. z , w >. e. v )
51	48, 50	bitri 264	. . . . . . . . . . 11 |- ( ( k X. { x } ) C_ v <-> A. z e. k A. w e. { x } <. z , w >. e. v )
52	47, 51	syl6bbr 278	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> ( A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> ( k X. { x } ) C_ v ) )
53	19, 34, 52	3bitrd 294	. . . . . . . . 9 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ x e. X ) -> ( ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } <-> ( k X. { x } ) C_ v ) )
54	53	rabbidva 3188	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } = { x e. X | ( k X. { x } ) C_ v } )
55		sneq 4187	. . . . . . . . . . . . . 14 |- ( x = w -> { x } = { w } )
56	55	xpeq2d 5139	. . . . . . . . . . . . 13 |- ( x = w -> ( k X. { x } ) = ( k X. { w } ) )
57	56	sseq1d 3632	. . . . . . . . . . . 12 |- ( x = w -> ( ( k X. { x } ) C_ v <-> ( k X. { w } ) C_ v ) )
58	57	elrab 3363	. . . . . . . . . . 11 |- ( w e. { x e. X | ( k X. { x } ) C_ v } <-> ( w e. X /\ ( k X. { w } ) C_ v ) )
59		eqid 2622	. . . . . . . . . . . . 13 |- U. ( S ↾t k ) = U. ( S ↾t k )
60		eqid 2622	. . . . . . . . . . . . 13 |- U. R = U. R
61		simplr 792	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( S ↾t k ) e. Comp )
62		simpll 790	. . . . . . . . . . . . . . 15 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) -> R e. (TopOn ` X ) )
63	62	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> R e. (TopOn ` X ) )
64		topontop 20718	. . . . . . . . . . . . . 14 |- ( R e. (TopOn ` X ) -> R e. Top )
65	63, 64	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> R e. Top )
66		topontop 20718	. . . . . . . . . . . . . . . . . 18 |- ( S e. (TopOn ` Y ) -> S e. Top )
67	66	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> S e. Top )
68	64	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> R e. Top )
69		txtop 21372	. . . . . . . . . . . . . . . . 17 |- ( ( S e. Top /\ R e. Top ) -> ( S tX R ) e. Top )
70	67, 68, 69	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( S tX R ) e. Top )
71	70	ad3antrrr 766	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( S tX R ) e. Top )
72		vex 3203	. . . . . . . . . . . . . . . 16 |- k e. _V
73		toponmax 20730	. . . . . . . . . . . . . . . . 17 |- ( R e. (TopOn ` X ) -> X e. R )
74	63, 73	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> X e. R )
75		xpexg 6960	. . . . . . . . . . . . . . . 16 |- ( ( k e. _V /\ X e. R ) -> ( k X. X ) e. _V )
76	72, 74, 75	sylancr 695	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. X ) e. _V )
77		simprr 796	. . . . . . . . . . . . . . . 16 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) -> v e. ( S tX R ) )
78	77	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> v e. ( S tX R ) )
79		elrestr 16089	. . . . . . . . . . . . . . 15 |- ( ( ( S tX R ) e. Top /\ ( k X. X ) e. _V /\ v e. ( S tX R ) ) -> ( v i^i ( k X. X ) ) e. ( ( S tX R ) ↾t ( k X. X ) ) )
80	71, 76, 78, 79	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( v i^i ( k X. X ) ) e. ( ( S tX R ) ↾t ( k X. X ) ) )
81	67	ad3antrrr 766	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> S e. Top )
82	72	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> k e. _V )
83		txrest 21434	. . . . . . . . . . . . . . . 16 |- ( ( ( S e. Top /\ R e. Top ) /\ ( k e. _V /\ X e. R ) ) -> ( ( S tX R ) ↾t ( k X. X ) ) = ( ( S ↾t k ) tX ( R ↾t X ) ) )
84	81, 65, 82, 74, 83	syl22anc 1327	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( ( S tX R ) ↾t ( k X. X ) ) = ( ( S ↾t k ) tX ( R ↾t X ) ) )
85		toponuni 20719	. . . . . . . . . . . . . . . . . . 19 |- ( R e. (TopOn ` X ) -> X = U. R )
86	63, 85	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> X = U. R )
87	86	oveq2d 6666	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( R ↾t X ) = ( R ↾t U. R ) )
88	60	restid 16094	. . . . . . . . . . . . . . . . . 18 |- ( R e. (TopOn ` X ) -> ( R ↾t U. R ) = R )
89	63, 88	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( R ↾t U. R ) = R )
90	87, 89	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( R ↾t X ) = R )
91	90	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( ( S ↾t k ) tX ( R ↾t X ) ) = ( ( S ↾t k ) tX R ) )
92	84, 91	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( ( S tX R ) ↾t ( k X. X ) ) = ( ( S ↾t k ) tX R ) )
93	80, 92	eleqtrd 2703	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( v i^i ( k X. X ) ) e. ( ( S ↾t k ) tX R ) )
94	23	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> S e. (TopOn ` Y ) )
95	26	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> k C_ Y )
96		resttopon 20965	. . . . . . . . . . . . . . . . 17 |- ( ( S e. (TopOn ` Y ) /\ k C_ Y ) -> ( S ↾t k ) e. (TopOn ` k ) )
97	94, 95, 96	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( S ↾t k ) e. (TopOn ` k ) )
98		toponuni 20719	. . . . . . . . . . . . . . . 16 |- ( ( S ↾t k ) e. (TopOn ` k ) -> k = U. ( S ↾t k ) )
99	97, 98	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> k = U. ( S ↾t k ) )
100	99	xpeq1d 5138	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) = ( U. ( S ↾t k ) X. { w } ) )
101		simprr 796	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) C_ v )
102		simprl 794	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> w e. X )
103	102	snssd 4340	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> { w } C_ X )
104		xpss2 5229	. . . . . . . . . . . . . . . 16 |- ( { w } C_ X -> ( k X. { w } ) C_ ( k X. X ) )
105	103, 104	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) C_ ( k X. X ) )
106	101, 105	ssind 3837	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) C_ ( v i^i ( k X. X ) ) )
107	100, 106	eqsstr3d 3640	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( U. ( S ↾t k ) X. { w } ) C_ ( v i^i ( k X. X ) ) )
108	102, 86	eleqtrd 2703	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> w e. U. R )
109	59, 60, 61, 65, 93, 107, 108	txtube 21443	. . . . . . . . . . . 12 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> E. r e. R ( w e. r /\ ( U. ( S ↾t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) )
110		toponss 20731	. . . . . . . . . . . . . . . . 17 |- ( ( R e. (TopOn ` X ) /\ r e. R ) -> r C_ X )
111	63, 110	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> r C_ X )
112		ssrab 3680	. . . . . . . . . . . . . . . . 17 |- ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> ( r C_ X /\ A. x e. r ( k X. { x } ) C_ v ) )
113	112	baib 944	. . . . . . . . . . . . . . . 16 |- ( r C_ X -> ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> A. x e. r ( k X. { x } ) C_ v ) )
114	111, 113	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> A. x e. r ( k X. { x } ) C_ v ) )
115		xpss2 5229	. . . . . . . . . . . . . . . . . 18 |- ( r C_ X -> ( k X. r ) C_ ( k X. X ) )
116	111, 115	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( k X. r ) C_ ( k X. X ) )
117	116	biantrud 528	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( ( k X. r ) C_ v <-> ( ( k X. r ) C_ v /\ ( k X. r ) C_ ( k X. X ) ) ) )
118		iunid 4575	. . . . . . . . . . . . . . . . . . . 20 |- U_ x e. r { x } = r
119	118	xpeq2i 5136	. . . . . . . . . . . . . . . . . . 19 |- ( k X. U_ x e. r { x } ) = ( k X. r )
120		xpiundi 5173	. . . . . . . . . . . . . . . . . . 19 |- ( k X. U_ x e. r { x } ) = U_ x e. r ( k X. { x } )
121	119, 120	eqtr3i 2646	. . . . . . . . . . . . . . . . . 18 |- ( k X. r ) = U_ x e. r ( k X. { x } )
122	121	sseq1i 3629	. . . . . . . . . . . . . . . . 17 |- ( ( k X. r ) C_ v <-> U_ x e. r ( k X. { x } ) C_ v )
123		iunss 4561	. . . . . . . . . . . . . . . . 17 |- ( U_ x e. r ( k X. { x } ) C_ v <-> A. x e. r ( k X. { x } ) C_ v )
124	122, 123	bitri 264	. . . . . . . . . . . . . . . 16 |- ( ( k X. r ) C_ v <-> A. x e. r ( k X. { x } ) C_ v )
125		ssin 3835	. . . . . . . . . . . . . . . 16 |- ( ( ( k X. r ) C_ v /\ ( k X. r ) C_ ( k X. X ) ) <-> ( k X. r ) C_ ( v i^i ( k X. X ) ) )
126	117, 124, 125	3bitr3g 302	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( A. x e. r ( k X. { x } ) C_ v <-> ( k X. r ) C_ ( v i^i ( k X. X ) ) ) )
127	99	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> k = U. ( S ↾t k ) )
128	127	xpeq1d 5138	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( k X. r ) = ( U. ( S ↾t k ) X. r ) )
129	128	sseq1d 3632	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( ( k X. r ) C_ ( v i^i ( k X. X ) ) <-> ( U. ( S ↾t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) )
130	114, 126, 129	3bitrd 294	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> ( U. ( S ↾t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) )
131	130	anbi2d 740	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) <-> ( w e. r /\ ( U. ( S ↾t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) ) )
132	131	rexbidva 3049	. . . . . . . . . . . 12 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) <-> E. r e. R ( w e. r /\ ( U. ( S ↾t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) ) )
133	109, 132	mpbird 247	. . . . . . . . . . 11 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) )
134	58, 133	sylan2b 492	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) /\ w e. { x e. X | ( k X. { x } ) C_ v } ) -> E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) )
135	134	ralrimiva 2966	. . . . . . . . 9 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> A. w e. { x e. X | ( k X. { x } ) C_ v } E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) )
136		eltop2 20779	. . . . . . . . . 10 |- ( R e. Top -> ( { x e. X | ( k X. { x } ) C_ v } e. R <-> A. w e. { x e. X | ( k X. { x } ) C_ v } E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) ) )
137	14, 68, 136	3syl 18	. . . . . . . . 9 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> ( { x e. X | ( k X. { x } ) C_ v } e. R <-> A. w e. { x e. X | ( k X. { x } ) C_ v } E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) ) )
138	135, 137	mpbird 247	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> { x e. X | ( k X. { x } ) C_ v } e. R )
139	54, 138	eqeltrd 2701	. . . . . . 7 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } e. R )
140		imaeq2 5462	. . . . . . . . 9 |- ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( `' F " z ) = ( `' F " { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) )
141	7	mptpreima 5628	. . . . . . . . 9 |- ( `' F " { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) = { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } }
142	140, 141	syl6eq 2672	. . . . . . . 8 |- ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( `' F " z ) = { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } )
143	142	eleq1d 2686	. . . . . . 7 |- ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( ( `' F " z ) e. R <-> { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } e. R ) )
144	139, 143	syl5ibrcom 237	. . . . . 6 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S ↾t k ) e. Comp ) -> ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( `' F " z ) e. R ) )
145	144	expimpd 629	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) -> ( ( ( S ↾t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) -> ( `' F " z ) e. R ) )
146	145	rexlimdvva 3038	. . . 4 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( E. k e. ~P U. S E. v e. ( S tX R ) ( ( S ↾t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) -> ( `' F " z ) e. R ) )
147	13, 146	syl5bi 232	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( z e. ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) -> ( `' F " z ) e. R ) )
148	147	ralrimiv 2965	. 2 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> A. z e. ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ( `' F " z ) e. R )
149		simpl 473	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> R e. (TopOn ` X ) )
150		ovex 6678	. . . . . 6 |- ( S Cn ( S tX R ) ) e. _V
151	150	pwex 4848	. . . . 5 |- ~P ( S Cn ( S tX R ) ) e. _V
152	9, 10, 11	xkotf 21388	. . . . . 6 |- ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) : ( { w e. ~P U. S | ( S ↾t w ) e. Comp } X. ( S tX R ) ) --> ~P ( S Cn ( S tX R ) )
153		frn 6053	. . . . . 6 |- ( ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) : ( { w e. ~P U. S | ( S ↾t w ) e. Comp } X. ( S tX R ) ) --> ~P ( S Cn ( S tX R ) ) -> ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) C_ ~P ( S Cn ( S tX R ) ) )
154	152, 153	ax-mp 5	. . . . 5 |- ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) C_ ~P ( S Cn ( S tX R ) )
155	151, 154	ssexi 4803	. . . 4 |- ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) e. _V
156	155	a1i 11	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) e. _V )
157	9, 10, 11	xkoval 21390	. . . 4 |- ( ( S e. Top /\ ( S tX R ) e. Top ) -> ( ( S tX R ) ^ko S ) = ( topGen ` ( fi ` ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ) ) )
158	67, 70, 157	syl2anc 693	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( ( S tX R ) ^ko S ) = ( topGen ` ( fi ` ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ) ) )
159		eqid 2622	. . . . 5 |- ( ( S tX R ) ^ko S ) = ( ( S tX R ) ^ko S )
160	159	xkotopon 21403	. . . 4 |- ( ( S e. Top /\ ( S tX R ) e. Top ) -> ( ( S tX R ) ^ko S ) e. (TopOn ` ( S Cn ( S tX R ) ) ) )
161	67, 70, 160	syl2anc 693	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( ( S tX R ) ^ko S ) e. (TopOn ` ( S Cn ( S tX R ) ) ) )
162	149, 156, 158, 161	subbascn 21058	. 2 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( F e. ( R Cn ( ( S tX R ) ^ko S ) ) <-> ( F : X --> ( S Cn ( S tX R ) ) /\ A. z e. ran ( k e. { w e. ~P U. S | ( S ↾t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ( `' F " z ) e. R ) ) )
163	8, 148, 162	mpbir2and 957	1 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> F e. ( R Cn ( ( S tX R ) ^ko S ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   <.cop 4183   U.cuni 4436   U_ciun 4520   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fun wfun 5882   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   ficfi 8316   ↾_t crest 16081   topGenctg 16098   Topctop 20698  TopOnctopon 20715   Cn ccn 21028   Compccmp 21189   tX ctx 21363   ^ko cxko 21364

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-cn 21031  df-cnp 21032  df-cmp 21190  df-tx 21365  df-xko 21366

This theorem is referenced by:  cnmpt2k  21491